Integrating formal specifications into applications: the ProB Java API
- PDF / 1,265,413 Bytes
- 28 Pages / 439.37 x 666.142 pts Page_size
- 66 Downloads / 224 Views
Integrating formal specifications into applications: the ProB Java API Philipp Körner1 · Jens Bendisposto1 · Jannik Dunkelau1 Sebastian Krings1 · Michael Leuschel1
·
Received: 12 March 2020 / Accepted: 29 September 2020 © The Author(s) 2020
Abstract 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, we propose a different approach: instead of generating code from formal models, it is also possible to embed a model checker or animator into applications in order to use the formal models themselves at runtime. We present a Java API to the ProB animator and model checker. We describe several case studies that use this API as enabling technology to interact with a formal specification at runtime. Keywords Formal methods · Run-time execution · Embedding · ProB · ProB Java API
1 Introduction When designing safety-critical software, the use of formal methods is highly recommended [18] to ensure correctness. This is often done by combining (manual and automatic) proof with model checking. Once a formal model has been found to be correct, it is usually required to translate the model into a traditional, imperative programming language. Then, low-level formalisms are usually close enough that code can be generated easily. When using high-level formalisms
B
Philipp Körner [email protected] Jens Bendisposto [email protected] Jannik Dunkelau [email protected] Sebastian Krings [email protected] Michael Leuschel [email protected]
1
Institut für Informatik, HHU Düsseldorf, Universitätsstr. 1, 40225 Düsseldorf, Germany
123
Formal Methods in System Design
though, the model has to be gradually refined to an implementation level so that it only uses a restricted version of the specification language, disallowing high-level constructs which require, e.g., constraint solving techniques or unconstrained memory for execution. The alternative to code generation is manual implementation, which is known to be error-prone. In this paper, we investigate another approach: we assume that a high-level specification is written to be executable, in the sense that a tool like an animator or model checker is able to compute all state transitions. Can we then implement a program interfacing with, e.g., a model checker that also simulates the environment and executes the model by choosing a traversing transition? This paper is a mixture of a position, tool and application paper, and is structured as follows: in the remainder of this section, we briefly introduce two high-level specification languages, B and Event-B, as well as ProB, an animator and model checker for these languages. Afterwards, we present the enabling technology, the ProB Java API, which allows for fine-grained interaction with ProB in Sect. 2. Following, we evaluate our approach by implementing and discussing several new case studies based on the ProB Java API in S
Data Loading...
