Course content

The course is about the software development process for reliable and safety-critical distributed reactive systems. In particular, students learn how to create such systems with abstract system models as a starting point via design synthesis to code generation and execution. In addition, we use the relatively easy formal modelling technique Temporal Logic of Actions (TLA) and its specification language TLA+ to specify safety-critical systems. Moreover, the TCL model checker will be applied to automatically verify that the development of more detailed systems based on more abstract ones is correct and that specific safety-critical properties are guaranteed. Finally, we discuss how safe systems can be properly tested.

The course consists of the following units:

Unit 1: Implementing State Machines (SMs)

• Introduction to the development of safety-critical systems.
• Get an overview about modeling such systems.
• Refresh your knowledge of state machine semantics, and how state machines can be implemented in code.

Unit 2: System Architecture and Standardized Development

• Get an understanding, how redundancy, reliability, and availability impact the safety of a system.
• Predict failure rates in 2oo3 and 2oo4 systems.
• Complying with Safety Criteria and Standards.

Unit 3: Towards Temporal Logic: The Notation TLA+

• Get an understanding about realizing state machines using the notation TLA+.
• Learn to make simple specifications in TLA+.
• Carry out first proofs of properties using the modelchecker TLC.

Unit 4:Temperal Logic of Actions (TLA)

• Understand temporal formulas and the difference between safety and liveness.
• Learn to specify and verify that one spefication is a refinement of another one (stepwise refinements).
• Carry out your stepwise refinement proofs with TLC.

Unit 5: Qualification of Safety System Software

• Get an overview about the process of licensing software.
• The verification and validation process of qualifying software.
• Design a larger example of a safety-critical system using the methods learned in the course.

Unit 6: Testing

• Learn about the main ideas and techniques for testing systems.

Learning outcome

A. Knowledge:

1. Software development process for safety-critical systems.
2. Model-based development methods to engineer reliable and safety-critical distributed reactive systems from abstract system models via design synthesis to code generation and execution.
3. Formal specification of safety-critical systems in an easily understandable temporal logic and automatic verification of system properties using model checkers.
4. System validation through testing.

B. Skills:

1. Use of selected UML-based modeling languages, methods and tools for specification, design, implementation and analysis of safety-critical systems.
2. Use of the specification language TLA+ to model system behavior. TLA+ is based on the Temporal Logic of Actions (TLA) and allows us to model systems quite similarly to programming languages.
3. Use of the TLC model checker which is also based on TLA to guarantee that the system models fulfill certain safety-critical properties and that a more detailed system is indeed an implementation of a more abstract one.
4. Practical development and execution of reliable systems that follow the general software development process for safety-critical systems.

C. General competence:

1. Applying the principles of software design to distributed safety-critical systems.
2. Basic understanding of the use of formal methods to specify and verify key properties of reliable systems.

The learning outcome of this course is related to the construction of safety-critical systems that will become the backbone of digital ecosystems, i.e., integrated distributed systems and other critical infrastructures. Such systems are important for society and must therefore implement functions in a robust, secure and efficient manner. Therefore, the outcome of this course is directly related to UN Sustainable Development Goal (SDG) 9 (Industry, Innovation and Infrastructure). The gained knowledge, skills, and competence also contribute indirectly to other SDGs as enablers in various domains, in particular to goal 2 (Zero Hunger), 3 (Good Health and Well-Being), 7 (Affordable Clean Energy), and 11 (Sustainable Cities and Communities).

Learning methods and activities

The course is taught according to the principle of team-based learning. It consists of individual work, group work and immediate feedback. The objective is to foster active student participation in the course. The principle is explained at www.teambasedlearning.org. Throughout the semester, students receive feedback on the learning process by several Readiness Assurance Tests (RATs), which also contribute to the final grade. To qualify for the final exam, a student has to reach at least 40% of the possible points in the readiness assurance tests.

Recommended previous knowledge

TTM4115 Design of Communicating Systems or equivalent.

Course materials

In this course, two primary resources are utilized:

1. Development of Safety-Critical Systems by Gopinath Karmakar, Amol Wakankar, Ashutosh Kabra, and Paritosh Pandya, accessible as an e-book through NTNU’s network; and
2. The TLA+ Video Course from Leslie Lamport, which is freely available online.

Credit reductions