Exploring a Methodology for Formal Verification of Safety-Critical Systems

Abstract

As the formal verification of safety-critical software systems often requires the integration of multiple tools and techniques, we propose a three-phase methodology incorporating two complementary workflows to ensure that the system in question fulfills its requirements. We use the Formal Requirements Elicitation Tool (FRET) to structure the requirements so that they can be translated to other formalisms. These translations are then either incorporated directly into an existing model in Simulink, or used to construct a new formal model of the system. Our current use case is a model of a controller for a civilian aircraft engine.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{Sheridan23,
  author       = {Ois{\'{\i}}n Sheridan},
  editor       = {Uwe Gl{\"{a}}sser and
                  Jos{\'{e}} Creissac Campos and
                  Dominique M{\'{e}}ry and
                  Philippe A. Palanque},
  title        = {Exploring a Methodology for Formal Verification of Safety-Critical
                  Systems},
  booktitle    = {Rigorous State-Based Methods - 9th International Conference, {ABZ}
                  2023, Nancy, France, May 30 - June 2, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14010},
  pages        = {361--365},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-33163-3\_26},
  doi          = {10.1007/978-3-031-33163-3\_26},
  timestamp    = {Fri, 02 Jun 2023 21:23:52 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/Sheridan23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}