Formalisation-Driven Development of Safety-Critical Systems

Alexei Iliasov, Alexander Romanovsky, Elena Troubitsyna, Linas Laibinis

    Forskningsoutput: Kapitel i bok/konferenshandlingKonferensbidragVetenskapligPeer review

    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åkOdefinierat/okänt
    Titel på gästpublikationIEEE 17th International Symposium on High Assurance Systems Engineering
    RedaktörerRadu Babiceanu, Helene Waeselynck, Raymond A. Paul, Bojan Cukic, Xu Jie
    FörlagIEEE
    Sidor165–172
    ISBN (tryckt)978-1-4673-9912-8
    DOI
    StatusPublicerad - 2016
    MoE-publikationstypA4 Artikel i en konferenspublikation
    EvenemangInternational Symposium on High Assurance Systems Engineering, HASE - HASE 2016: 17th International Symposium on High Assurance Systems Engineering
    Varaktighet: 7 jan 20169 jan 2016

    Konferens

    KonferensInternational Symposium on High Assurance Systems Engineering, HASE
    Period07/01/1609/01/16

    Citera det här