Formal Verification of Event-driven Health Applications

Mohammad-Reza Gholami, Hanifa Boucheneb


Software does an important task in almost every part of our everyday life, particularly in systems designed for the healthcare, aircraft navigation and automotive. One of the important objectives of software engineering is to support developers for building systems that function reliably even they are complex. In this paper, we show how Model-Based Design is used to model a safety-related application. By applying formal verification techniques, we also define specific properties to ensure that a software system satisfies its correctness criteria. We use the formal approach to study and verify the properties of a medical device known as Endotracheal intubation. The system is modeled in a concurrent manner and synchronization between components is done through events. We present how the system is modeled in the Simulink and Stateflow and present formalization of some safety and temporal requirements based on the events issued from the controller. In order to formally prove the defined properties, we employ Simulink Design Verifier toolset.


Formal Methods; Formal Verification; Design Verification; Model-Based Design; Linear Temporal Logic; Safety-Critical

Full Text:




  • There are currently no refbacks.

ISSN: 2377-3316

CC BY Google Scholar DOAJ  Crossref logo