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

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussa › Konferenssiartikkeli › Tieteellinen › vertaisarvioitu

1 Sitaatiot (Scopus)

Abstrakti

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.

Alkuperäiskieli	Ei tiedossa
Otsikko	IEEE 17th International Symposium on High Assurance Systems Engineering
Toimittajat	Radu Babiceanu, Helene Waeselynck, Raymond A. Paul, Bojan Cukic, Xu Jie
Kustantaja	IEEE
Sivut	165–172
ISBN (painettu)	978-1-4673-9912-8
DOI - pysyväislinkit	https://doi.org/10.1109/HASE.2016.35
Tila	Julkaistu - 2016
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisuussa
Tapahtuma	International Symposium on High Assurance Systems Engineering, HASE - HASE 2016: 17th International Symposium on High Assurance Systems Engineering Kesto: 7 tammik. 2016 → 9 tammik. 2016

Konferenssi

Konferenssi	International Symposium on High Assurance Systems Engineering, HASE
Ajanjakso	07/01/16 → 09/01/16

Pääsy asiakirjaan

10.1109/HASE.2016.35

Viittausmuodot

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

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussa › Konferenssiartikkeli › Tieteellinen › vertaisarvioitu

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 -