Formal methods have an important role in ensuring the correctness of safety critical systems. However, their application in industry is always cumbersome: the lack of experts and the complexity of formal languages prevents the efficient application of formal verification techniques. In this paper we take a step in the direction of making formal modelling simpler by introducing a framework which helps designers to construct formal models efficiently. Our formal modelling framework supports the development of traditional transition systems enriched with complex data types with type checking and type inference services, time dependent behaviour and timing parameters with relations. In addition, we introduce a toolchain to provide formal verification. Finally, we demonstrate the usefulness of our approach in an industrial case study. © 2014 Springer International Publishing.
CITATION STYLE
Tóth, T., Vörös, A., & Majzik, I. (2014). Verification of a real-time safety-critical protocol using a modelling language with formal data and behaviour semantics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8696 LNCS, pp. 207–218). Springer Verlag. https://doi.org/10.1007/978-3-319-10557-4_24
Mendeley helps you to discover research relevant for your work.