The Refinement Calculus of Reactive Systems Toolset
- PDF / 1,625,697 Bytes
- 20 Pages / 595.276 x 790.866 pts Page_size
- 38 Downloads / 175 Views
STTT Special Issue TACAS 2018
The Refinement Calculus of Reactive Systems Toolset Iulia Dragomir1 · Viorel Preoteasa2 · Stavros Tripakis3
© Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract We present the Refinement Calculus of Reactive Systems Toolset, an environment for compositional formal modeling and reasoning about reactive systems, built around Isabelle, Simulink, and Python. The toolset implements the Refinement Calculus of Reactive Systems (RCRS), a contract-based refinement framework inspired by the classic refinement calculus and interface theories. The toolset formalizes the entire RCRS theory in about 30000 lines of Isabelle code. The toolset also contains a translator of Simulink diagrams and a formal analyzer implemented on top of Isabelle. We present the main functionalities of the RCRS Toolset via a series of pedagogical examples and also describe a larger case study from the automotive domain. Keywords Block diagrams · Compositionality · Refinement · Contract synthesis · Formal verification · Theorem proving · Isabelle · Simulink
1 Introduction The Refinement Calculus of Reactive Systems (RCRS) is a compositional framework for modeling and reasoning about reactive systems. One of the motivations behind RCRS has been to model and formally reason about industrial strength systems, for instance, those modeled in the widespread Simulink environment by the MathWorks. RCRS has been inspired by component-based frameworks such as interface automata [9] and has its origins in the theory of relational interfaces [41], but also borrows from the classic refinement calculus [4]. RCRS allows compositional modeling of input–output systems which are both non-deterministic (meaning that for a given input, there could be many possible outputs) and noninput-receptive (meaning that some inputs are illegal). Being
B
Stavros Tripakis [email protected] Iulia Dragomir [email protected] Viorel Preoteasa [email protected]
1
GMV Aerospace and Defence SAU, Madrid, Spain
2
Huld, Espoo, Finland
3
Northeastern University, Boston, MA, USA
able to model systems that have both these characteristics in turn enables static analysis similar to type checking [41,43]. The ability to model systems which are both nondeterministic and non-input-receptive is also present in the theory of relational interfaces. But relational interfaces are limited to safety properties. The main motivation behind RCRS has been to lift this limitation and to be able to describe both safety and liveness properties. This has been achieved by abandoning the relational semantics of relational interfaces and adopting the much more powerful semantics of the refinement calculus (RC) [4]. RC is a compositional modeling and verification framework for sequential programs. RCRS extends RC to reactive systems. One of the main ideas is to adapt the semantics of RC, which is based on predicate transformers [11], to property transformers which are suitable for expressing dynamic behaviors. The theory of RCRS has been introduce
Data Loading...
