Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Dependable Architectures and Software

Description

This lecture covers the concept of dependable architectures, error detection, fault-tolerant structures, and issues in workby and standby implementations. It delves into error detection methods, physical fault detection, and the importance of watchdog processors. The lecture also discusses the Byzantine Generals' Problem, the Patriot Missile failure, and examples of dependable architectures like ABB dual controller and Boeing 777 Primary Flight Control. Furthermore, it explores the importance of formal verification, testing, and recovery blocks in ensuring software dependability.

This video is available exclusively on Mediaspace for a restricted audience. Please log in to MediaSpace to access it if you have the necessary permissions.

Watch on Mediaspace

Instructor

Jean-Charles Tournier

Official source

Related concepts (32)

Fault tolerance

Fault tolerance is the property that enables a system to continue operating properly in the event of the failure of one or more faults within some of its components. If its operating quality decreases at all, the decrease is proportional to the severity of the failure, as compared to a naively designed system, in which even a small failure can cause total breakdown. Fault tolerance is particularly sought after in high-availability, mission-critical, or even life-critical systems.

Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Formal methods

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Formal specification

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.

Reliability engineering

Reliability engineering is a sub-discipline of systems engineering that emphasizes the ability of equipment to function without failure. Reliability describes the ability of a system or component to function under stated conditions for a specified period of time. Reliability is closely related to availability, which is typically described as the ability of a component or system to function at a specified moment or interval of time. The reliability function is theoretically defined as the probability of success at time t, which is denoted R(t).

Related lectures (30)

Introduction to Formal Verification

Introduces formal verification, emphasizing rigorous proof of system correctness and the use of mathematical models.

Automated Testing: Fuzzing and Sanitization

Explores fuzzing, bug oracles, code reviews, and automated testing techniques, emphasizing the importance of sanitization in detecting faults.

Compiler verification: Challenges and Benefits

Explores the challenges and benefits of compiler verification, emphasizing the importance of verifying compilers for critical software.

From Tests to Proof

Explores software engineering concepts, emphasizing the significance of tests and clear specifications in ensuring software correctness.

Correctness of Compilers: Part 1