In this article, we present an approach to the ABZ 2020 case study, that differs from the ones usually presented at ABZ: Rather than using a (correct-by-construction) pproach following a formal method, we use MISRA C for a low-level implementation …
In this article, we present a concrete realisation of the ETCS Hybrid Level 3 concept, whose practical viability was evaluated in a field demonstration in 2017. Hybrid Level 3 introduces virtual sub-sections as sub-divisions of classical track …
In this article, we introduce a denotational translation of the specification language Alloy to classical B. Our translation closely follows the Alloy grammar. Each construct is translated into a semantically equivalent component of the B language. …
Courses on formal methods are often based on examples and case studies, supposed to show students how to apply formal methods in practice. However, examples often fall into one of two categories: First, many are artificial and thus do not relate to …
The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code. In this paper, …