Source: http://rcrs.cs.aalto.fi/
Timestamp: 2019-04-21 06:42:19+00:00

Document:
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.
RCRS has been fully formalized in the Isabelle theorem prover. This formalization is included in the publicly available RCRS Toolset (see below).
The RCRS Toolset comes with a Translator of Hierarchical Block Diagrams (Simulink).
The RCRS Toolset has been used on non-trivial examples, including a Fuel Control System benchmark provided by Toyota.
TACAS 2018 Distinguished Artifact Award!
TACAS 2018 Artifact Evaluation Badge!
The RCRS TACAS 2018 Artifact is available for download on figshare.
The implementation of the RCRS theory in Isabelle. You can browse the RCRS Isabelle theories.
A Formal Analyzer, implemented on top of Isabelle, which allows to perform compatibility checks on a model, to flatten and simplify a hierarchical model into a single monolithic symbolic transition system without internal variables ("wires"), and to generate simulation code.
The simulink2isabelle Translator, which translates Simulink models into RCRS Isabelle theories that can be processed by the Formal Analyzer. We support a decent subset of Simulink's basic blocks, including continuous-time blocks like Integrators.
A set of examples, including some toy Simulink models, and the theories generated by simulink2isabelle from the Fuel Control System benchmark. This benchmark is not included in our distribution (as it has been developed by a third party, Toyota) but it can be obtained from Benchmarks for Model Transformations and Conformance Checking.
To install, download the distribution (zip file) and read the README file. The simulink2isabelle Translator is written in Python and requires the third-party component pyparsing.
I. Dragomir, V. Preoteasa, S.Tripakis. The Refinement Calculus of Reactive Systems Toolset. TACAS 2018. Extended version in arXiv 2018. Distinguished Artifact Award.
V. Preoteasa, I. Dragomir, S.Tripakis. Mechanically Proving Determinacy of Hierarchical Block Diagram Translations. arXiv 2018.
V. Preoteasa, I. Dragomir, S.Tripakis. The Refinement Calculus of Reactive Systems. arXiv 2017.
V. Preoteasa, I. Dragomir, S.Tripakis. Type Inference of Simulink Hierarchical Block Diagrams in Isabelle. FORTE 2017.
V. Preoteasa, S.Tripakis. Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. LICS 2016.
S.Tripakis. Compositionality in the Science of System Design. Proceedings of the IEEE 2016.
I. Dragomir, V. Preoteasa, S.Tripakis. Compositional Semantics and Analysis of Hierarchical Block Diagrams. SPIN 2016.
V. Preoteasa, S.Tripakis. Refinement Calculus of Reactive Systems. EMSOFT 2014.
V. Preoteasa. Formalization of Refinement Calculus for Reactive Systems. Archive of Formal Proofs 2014.
S. Tripakis, C. Stergiou, M. Broy, E. A. Lee. Error-Completion in Interface Theories. SPIN 2013.
S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. A Theory of Synchronous Relational Interfaces. ACM TOPLAS 2011.
S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. On Relational Interfaces. EMSOFT 2009.
Academy of Finland research project 265939.
NSF CPS Breakthrough award CNS-1329759.
For any enquiries, you can contact us by email.

References: V. 

V. 

V. 

V. 

V. 
 V. 

V. 

V.