Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Formalisation-Driven Developme...

Formalisation-Driven Development of Safety-Critical Systems

Alexei Iliasov, Alexander Romanovsky, Elena Troubitsyna, Linas Laibinis, Formalisation-Driven Development of Safety-Critical Systems. In: Radu Babiceanu, Helene Waeselynck (Eds.), HASE 2016 -- IEEE High Assurance Systems Engineering Symposium, 165–172, IEEE, 2016.

http://dx.doi.org/10.1109/HASE.2016.35

Abstract:

The use of formal modelling and verification is recommended by several standards in the development of highly critical systems. However, the standards do not prescribe a process that enables a seamless integration of formalisation activities into the development process. In this paper, we propose a model and an automated tool support for an iterative formalisation-driven development of safety-critical systems in the Event-B framework. Event-B supports correct-by-construction development and provides the designers with a continuous feedback on the correctness of models and corresponding system requirements, including safety. To automate the proposed formalisation-driven development, we present a prototype of an automated tool support relying on the novel OSLC technology. It allows us to seamlessly integrate derivation of system requirements with formal modelling and proof-based verification.

BibTeX entry:

@INPROCEEDINGS{inpIlRoTrLa16a,
  title = {Formalisation-Driven Development of Safety-Critical Systems},
  booktitle = {HASE 2016 -- IEEE High Assurance Systems Engineering Symposium},
  author = {Iliasov, Alexei and Romanovsky, Alexander and Troubitsyna, Elena and Laibinis, Linas},
  editor = {Babiceanu, Radu and Waeselynck, Helene},
  publisher = {IEEE},
  pages = {165–172},
  year = {2016},
  keywords = {safety-critical systems, requirements, formal modelling, formal verification, OSLC},
  ISSN = {1530-2059/16},
}

Belongs to TUCS Research Unit(s): Embedded Systems Laboratory (ESLAB)

Edit publication