RCRS (the Refinement Calculus of Reactive Systems)
is a compositional reasoning framework:
RCRS can model open (input-output), non-deterministic, and non-input-receptive systems.
Non-deterministic means for a given input, many outputs may be possible. Non-input-receptive means some inputs may be declared as illegal.
Components can be specified as symbolic transition systems
or as temporal logic (LTL) formulas.
Components can be composed using three primitive operators:
serial, parallel, and feedback composition.
RCRS supports checking compatibility of components during composition.
RCRS supports refinement, which allows to reason about component substitutability.
RCRS supports both safety and liveness properties.
An implementation of the RCRS theory into the Isabelle theorem prover. The current implementation of the RCRS theory is compatible with Isabelle2016-1, downloadable from here.
The Simulink2Isabelle compiler, which translates
Simulink models
(hierarchical block diagrams) into RCRS.
We support a large subset of Simulink's basic blocks, including
continuous-time blocks like Integrators.
The tool chain is illustrated below. The tools currently allow to perform
compatibility checks on a model, to simplify the entire hierarchical model into a
single, monolithic symbolic transition system, and to generate simulation code
in Python. See our SPIN 2016 paper for details.
To install, download the distribution (zip file) and read the
README file. The Simulink2Isabelle is written in Python and relies on the
third-party component:
V. Preoteasa, I. Dragomir, S.Tripakis. Type Inference of Simulink Hierarchical Block Diagrams in Isabelle. arXiv, 2016 [paper]
V. Preoteasa, I. Dragomir, S.Tripakis. A Nondeterministic and Abstract Algorithm for Translating Hierarchical Block Diagrams. arXiv, 2016 [paper]
V. Preoteasa, S.Tripakis. Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. LICS 2016 [paper][technical report]
I. Dragomir, V. Preoteasa, S.Tripakis. Compositional Semantics and Analysis of Hierarchical Block Diagrams. SPIN 2016 [paper][technical report][slides]
V. Preoteasa, S.Tripakis. Refinement Calculus of Reactive Systems. EMSOFT 2014 [paper][technical report]
V. Preoteasa. Formalization of Refinement Calculus for Reactive Systems. Archive of Formal Proofs 2014 [paper][source]
S. Tripakis, C. Stergiou, M. Broy, E. A. Lee. Error-Completion in Interface Theories. SPIN 2013 [paper]
S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. A Theory of Synchronous Relational Interfaces. ACM TOPLAS 2011 [paper]
S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. On Relational Interfaces. EMSOFT 2009 [paper]