Runtime verification of reactive systems (a pacemaker case study)

Potential supervisors: 
Description: 

 

Runtime verification

Runtime verification refers to the theories, techniques, and tools that allow checking whether a run of a system under scrutiny satisfies (or violates) a given correctness property.

It is a formal verification technique, complementing the other formal verification techniques such as model checking. Runtime verification techniques do not influence the program execution, and deals only with detection of violation (or satisfaction) of properties. In runtime verification, checking whether a run of a system satisfies a property is performed using a monitor. A verification monitor is a decision procedure emitting verdicts stating the correctness of the (partial) observed trace generated from the system execution.

A central concept in runtime verification is to generate monitors from some high-level specification of the property which the monitor should check/verify. Monitors are generated from specifications such as Linear Temporal Logic (LTL), and automata.

Cardiac Pacemakers

The heart-pacemaker system is an example of Cyber Physical System (CPS), comprising a plant (the heart) and the controller (the pacemaker). Cardiac pacemakers are implantable medical devices designed to correct any dysfunction of the heart’s timing, known as arrythmias. As life-critical devices, pacemakers are extensively tested and verified, but not all faults can be discovered and corrected during development. In 2009, 4960 patients died as a result of software faults in pacemakers. Pacemakers use many different internal timers to check that pacing is correct, preventing completely exhaustive model checking because of state space explosion.

The project

The problem of synthesis of runtime verification monitors from properties has been extensively studied. The project involves application of existing RV mechanisms and tools to the pacemaker problem:

  • Identify crucial safety properties,
  • Formalizing the properties,
  • Explore existing monitor synthesis tools and generate monitors,
  • The student(s) may also be provided real models/source code of pacemaker programs (by our collaborators in Unvi. of Auckland, PERTzel group), and (or) data that can be used for off-line analysis,
  • Apply/use the synthesized monitors for off-line analysis,
  • Integrate monitors for on-line runtime verification.

Related courses: Finite automata theory and formal languages, Formal Methods in Software Development.

Prerequisites: Programming (C, Python,..), propositional logic, automata theory.

Desired: Temporal logics and formal verification, formal modelling and verification tools, Matlab.

Contact: Srinivas Pinisetty (sripin@chalmers.se) and Gerardo Schneider (gersch@chalmers.se)

 

 

Date range: 
October, 2017 to October, 2022