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 | |
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 |