This white paper argues that formal methods need to be better rooted in higher education curricula for computer science and software engineering programmes of study.
The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques.
The B-Method has an interesting history, where language and tools have evolved over the years.
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 instead.
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.
In this article, we introduce a denotational translation of the specification language Alloy to classical B.
iFM 2019, Bergen, Norway
FMFun 2019, Bergen, Norway
FMFun 2019, Bergen, Norway
Courses on formal methods are often based on examples and case studies, supposed to show students how to apply formal methods in practice.
The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques.
The B method for software and systems development together with the specification language B and its successor Event-B offer a rich history.
Employing formal methods for software development usually involves using a multitude of tools such as model checkers and provers.
During a course on model checking we developed BMoth, a full-stack model checker for classical B, featuring both explicit-state and symbolic model checking.
In this paper, we introduce a translation of the specification language Alloy to classical B.
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.
In general, even though Prolog is a dynamically typed language, predicates may not be called with arbitrarily typed arguments.
The idea of verifying the correctness of software has been brought up in the early days of computing, for example by Alan Turing in 1949 or Robert W.
Symbolic model checking algorithms like IC3 have proven to be an effective technique for hardware model checking.
The ProB disprover uses constraint solving to find counter-examples for B proof obligations.