This is an interdisciplinary course inspired by software engineering and formal methods. However, this course has been adapted for applicability for computer systems engineering, mechatronics, bio- engineering and medical devices domains. Executable biology refers to executable computational models that mimic biological processes. In this course we will present a range of executable models inspired by formal methods especially for medical device validation. The range of formal methods considered here include a synchronous Statechart called SCChart for pacemaker modelling, a long with a number of tools for formal verification such as: (1) Uppaal for pacemaker verification, (2) easy-rte for runtime verification and validation, (3) SPIN, which will be used for model checking concurrent programs, and finally (4) Satisfiability Modulo Theory based tool called Z3 from Microsoft, which will be used for program equivalence checking.
The course is taught in two parts:
Part 1-Fundamentals of model-based design founded on formal methods.
• Automatic verification of closed and open systems using model checking and module checking.
• Modelling and verification of a pacemaker using UPPAAL.
• Run-time verification and enforcement of safety-critical systems.
• Formal modelling and verification using process algebras and bisimulation.
• Introduction to Cyber-Physical Systems (CPS).
Part 2-Industrial successes of formal methods
• Linear Temporal Logic and its industrial applications
• Satisfiability Modulo Theory
• Proof carrying code
• Correctness of software programs