Refinement Calculus of Reactive Systems

RCRS (the Refinement Calculus of Reactive Systems) is a compositional reasoning framework:

Download

Latest version distributed under the MIT license.

The RCRS Toolset

The RCRS Toolset currently includes:



Installation

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.

Awards

TACAS 2018 Distinguished Artifact Award TACAS 2018 Artifact Evaluation Badge

Papers

  1. I. Dragomir, V. Preoteasa, S.Tripakis. The Refinement Calculus of Reactive Systems Toolset. STTT 2020.
    [paper]
  2. V. Preoteasa, T. Latvala, K. Varpaaniemi. Modelling Programmable Logic Controllers in Refinement Calculus of Reactive Systems. CS&P 2019.
    [paper]
  3. V. Preoteasa, I. Dragomir, S.Tripakis. Mechanically Proving Determinacy of Hierarchical Block Diagram Translations. VMCAI 2019. Extended version in arXiv 2018.
    [paper]  [technical report]
  4. I. Dragomir, V. Preoteasa, S.Tripakis. The Refinement Calculus of Reactive Systems Toolset. TACAS 2018. Extended version in arXiv 2018. Distinguished Artifact Award.
    [paper]  [technical report] 
  5. V. Preoteasa, I. Dragomir, S.Tripakis. The Refinement Calculus of Reactive Systems. arXiv 2017.
    [technical report] 
  6. V. Preoteasa, I. Dragomir, S.Tripakis. Type Inference of Simulink Hierarchical Block Diagrams in Isabelle. FORTE 2017.
    [paper]  [technical report]  [slides]
  7. V. Preoteasa, S.Tripakis. Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. LICS 2016.
    [paper]  [technical report]
  8. S.Tripakis. Compositionality in the Science of System Design. Proceedings of the IEEE 2016.
    [paper]
  9. I. Dragomir, V. Preoteasa, S.Tripakis. Compositional Semantics and Analysis of Hierarchical Block Diagrams. SPIN 2016.
    [paper]  [technical report]  [slides]
  10. V. Preoteasa, S.Tripakis. Refinement Calculus of Reactive Systems. EMSOFT 2014.
    [paper]  [technical report]
  11. V. Preoteasa. Formalization of Refinement Calculus for Reactive Systems. Archive of Formal Proofs 2014.
    [paper]  [source]
  12. S. Tripakis, C. Stergiou, M. Broy, E. A. Lee. Error-Completion in Interface Theories. SPIN 2013.
    [paper]
  13. S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. A Theory of Synchronous Relational Interfaces. ACM TOPLAS 2011.
    [paper]
  14. S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. On Relational Interfaces. EMSOFT 2009.
    [paper]

People


Sponsors

The RCRS project has been sponsored by:
For any enquiries, you can contact us by email.