Formalisation-Driven Development of Safety-Critical Systems

Alexei Iliasov; Alexander Romanovsky; Elena Troubitsyna; Linas Laibinis

doi:10.1109/HASE.2016.35

Formalisation-Driven Development of Safety-Critical Systems

Alexei Iliasov
, Alexander Romanovsky
, Elena Troubitsyna
, Linas Laibinis

Forskningsoutput: Kapitel i bok/konferenshandling › Publicerad konferensartikel › Vetenskaplig › Peer review

1 Citeringar (Scopus)

Sammanfattning

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 pro- cess 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 develop- ment and provides the designers with a continuous feedback on the correctness of models and corresponding system require- ments, 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.

Originalspråk	Odefinierat/okänt
Titel på värdpublikation	IEEE 17th International Symposium on High Assurance Systems Engineering
Redaktörer	Radu Babiceanu, Helene Waeselynck, Raymond A. Paul, Bojan Cukic, Xu Jie
Förlag	IEEE
Sidor	165–172
ISBN (tryckt)	978-1-4673-9912-8
DOI	https://doi.org/10.1109/HASE.2016.35
Status	Publicerad - 2016
MoE-publikationstyp	A4 Artikel i en konferenspublikation
Evenemang	International Symposium on High Assurance Systems Engineering, HASE - HASE 2016: 17th International Symposium on High Assurance Systems Engineering Varaktighet: 7 jan. 2016 → 9 jan. 2016

Konferens

Konferens	International Symposium on High Assurance Systems Engineering, HASE
Period	07/01/16 → 09/01/16

Åtkomst av dokument

10.1109/HASE.2016.35

Citera det här

@inproceedings{6baaf9bda7d843368ef32f825a5fd361,

title = "Formalisation-Driven Development of Safety-Critical Systems",

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 pro- cess 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 develop- ment and provides the designers with a continuous feedback on the correctness of models and corresponding system require- ments, 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. ",

author = "Alexei Iliasov and Alexander Romanovsky and Elena Troubitsyna and Linas Laibinis",

year = "2016",

doi = "10.1109/HASE.2016.35",

language = "Odefinierat/ok{\"a}nt",

isbn = "978-1-4673-9912-8",

pages = "165–172",

editor = "Radu Babiceanu and Helene Waeselynck and Paul, \{Raymond A.\} and Bojan Cukic and Xu Jie",

booktitle = "IEEE 17th International Symposium on High Assurance Systems Engineering",

publisher = "IEEE",

note = "International Symposium on High Assurance Systems Engineering, HASE ; Conference date: 07-01-2016 Through 09-01-2016",

}

Iliasov, A, Romanovsky, A, Troubitsyna, E & Laibinis, L 2016, Formalisation-Driven Development of Safety-Critical Systems. i R Babiceanu, H Waeselynck, RA Paul, B Cukic & X Jie (red), IEEE 17th International Symposium on High Assurance Systems Engineering. IEEE, s. 165–172, International Symposium on High Assurance Systems Engineering, HASE, 07/01/16. https://doi.org/10.1109/HASE.2016.35

Formalisation-Driven Development of Safety-Critical Systems. / Iliasov, Alexei; Romanovsky, Alexander; Troubitsyna, Elena et al.
IEEE 17th International Symposium on High Assurance Systems Engineering. red. / Radu Babiceanu; Helene Waeselynck; Raymond A. Paul; Bojan Cukic; Xu Jie. IEEE, 2016. s. 165–172.

Forskningsoutput: Kapitel i bok/konferenshandling › Publicerad konferensartikel › Vetenskaplig › Peer review

TY - GEN

T1 - Formalisation-Driven Development of Safety-Critical Systems

AU - Iliasov, Alexei

AU - Romanovsky, Alexander

AU - Troubitsyna, Elena

AU - Laibinis, Linas

PY - 2016

Y1 - 2016

N2 - 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 pro- cess 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 develop- ment and provides the designers with a continuous feedback on the correctness of models and corresponding system require- ments, 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.

AB - 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 pro- cess 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 develop- ment and provides the designers with a continuous feedback on the correctness of models and corresponding system require- ments, 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.

U2 - 10.1109/HASE.2016.35

DO - 10.1109/HASE.2016.35

M3 - Publicerad konferensartikel

SN - 978-1-4673-9912-8

SP - 165

EP - 172

BT - IEEE 17th International Symposium on High Assurance Systems Engineering

A2 - Babiceanu, Radu

A2 - Waeselynck, Helene

A2 - Paul, Raymond A.

A2 - Cukic, Bojan

A2 - Jie, Xu

PB - IEEE

T2 - International Symposium on High Assurance Systems Engineering, HASE

Y2 - 7 January 2016 through 9 January 2016

ER -