Applying Formal Methods into Safety-Critical Health Applications

  • Mohammad-Reza Gholami
  • Hanifa Boucheneb
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8822)


Software performs a critical role in almost every aspect of our daily life specially in the embedded systems of medical equipments. A key goal of software engineering is to make it possible for developers to construct systems that operate reliably regardless of their complexity. In this paper, by employing Model-Based Design for large and safety-related applications and applying formal verification techniques, we 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. We present how the system is modeled in the Simulink and Stateflow and present a functionality formalization. In order to formally prove some critical properties, we employ Simulink Design Verifier toolset.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Intensive care hotline, intubation,
  2. 2.
    Prover plug-in, prover,
  3. 3.
    User’s guide, the mathworks,
  4. 4.
    Alagar, V.S., Periyasamy, K.: Specification of software systems. Springer-Verlag New York Inc. (2011)Google Scholar
  5. 5.
    Behboodian, A.: Model-based design. DSP Magazine (May 2006)Google Scholar
  6. 6.
    Bjesse, P.: What is formal verification? ACM SIGDA Newsletter 35(24), 1 (2005)CrossRefGoogle Scholar
  7. 7.
    Denney, E., Trac, S.: A software safety certification tool for automatically generated guidance, navigation and control code. In: IEEE Aerospace Conference, pp. 1–11. IEEE (2008)Google Scholar
  8. 8.
    Etienne, J.F., Fechter, S., Juppeaux, E.: Using simulink design verifier for proving behavioral properties on a complex safety critical system in the ground transportation domain. In: Complex Systems Design & Management, pp. 61–72 (2010)CrossRefGoogle Scholar
  9. 9.
    Fey, I., Mller, J., Conrad, M.: Model-based design for safety-related applications. In: Proceedings of SAE Convergence (2008)Google Scholar
  10. 10.
    Fowler, M.: UML distilled: A brief guide to the standard object modeling language. Addison-Wesley Professional (2004)Google Scholar
  11. 11.
    Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)MathSciNetCrossRefGoogle Scholar
  12. 12.
    He, X., Ma, Z., Shao, W., Li, G.: A metamodel for the notation of graphical modeling languages. In: 31st Annual International Computer Software and Applications Conference, COMPSAC 2007, vol. 1, pp. 219–224. IEEE (2007)Google Scholar
  13. 13.
    Jiang, Z., Pajic, M., Connolly, A., Dixit, S., Mangharam, R.: Real-time heart model for implantable cardiac device validation and verification. In: 2010 22nd Euromicro Conference on Real-Time Systems (ECRTS), pp. 239–248. IEEE (2010)Google Scholar
  14. 14.
    Krasner, J.: Model-based design and beyond: Solutions for todays embedded systems requirements. Technical report, Mathworks (2004)Google Scholar
  15. 15.
    Friedman, J., Anthony, M.: Model-based design for large safety-critical systems: A discussion regarding model architecture. Technical report, MathworksGoogle Scholar
  16. 16.
    Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl M.P.E.: Compositional verification of a medical device system. In: Proceedings of the 2013 ACM SIGAda Annual Conference on High Integrity Language Technology, pp. 51–64. ACM (2013)Google Scholar
  17. 17.
    Popovici, K., Lalo, M.: Formal model and code verification in model-based design. In: Joint IEEE North-East Workshop on Circuits and Systems and TAISA Conference, NEWCAS-TAISA 2009, pp. 1–4. IEEE (2009)Google Scholar
  18. 18.
    Portugal, P., Carvalho, A.: The grafcet specification (2005)Google Scholar
  19. 19.
    Rushby, J.: Formal methods and the certification of critical systems. SRI International, Computer Science Laboratory (1993)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Mohammad-Reza Gholami
    • 1
  • Hanifa Boucheneb
    • 1
  1. 1.VeriForm Lab, Department of Computer and Software EngineeringEcole Polytechnique of MontrealCanada

Personalised recommendations