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 tool called Uppaal for pacemaker verification and a tool called Piha for the design of the cardiac conduction system, which will be validated using the SPIN model checker.
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