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

Research output: Chapter in Book/Conference proceeding › Conference contribution › Scientific › peer-review

1 Citation (Scopus)

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.

Original language	Undefined/Unknown
Title of host publication	IEEE 17th International Symposium on High Assurance Systems Engineering
Editors	Radu Babiceanu, Helene Waeselynck, Raymond A. Paul, Bojan Cukic, Xu Jie
Publisher	IEEE
Pages	165–172
ISBN (Print)	978-1-4673-9912-8
DOIs	https://doi.org/10.1109/HASE.2016.35
Publication status	Published - 2016
MoE publication type	A4 Article in a conference publication
Event	International Symposium on High Assurance Systems Engineering, HASE - HASE 2016: 17th International Symposium on High Assurance Systems Engineering Duration: 7 Jan 2016 → 9 Jan 2016

Conference

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

Access to Document

10.1109/HASE.2016.35

Cite this

@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. in R Babiceanu, H Waeselynck, RA Paul, B Cukic & X Jie (eds), IEEE 17th International Symposium on High Assurance Systems Engineering. IEEE, pp. 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. ed. / Radu Babiceanu; Helene Waeselynck; Raymond A. Paul; Bojan Cukic; Xu Jie. IEEE, 2016. p. 165–172.

Research output: Chapter in Book/Conference proceeding › Conference contribution › Scientific › 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 - Konferensbidrag

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 -