Refinement Calculus of Reactive Systems

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


The RCRS Toolset: Implementation and Download


Our group is developing and distributing (under the MIT license) the RCRS Toolset. The distribution currently includes:


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.

Papers


  1. I. Dragomir, V. Preoteasa, S.Tripakis. The Refinement Calculus of Reactive Systems Toolset. arXiv 2017. To appear also in TACAS 2018.
    [technical report] 
  2. V. Preoteasa, I. Dragomir, S.Tripakis. The Refinement Calculus of Reactive Systems. arXiv 2017
    [technical report] 
  3. V. Preoteasa, I. Dragomir, S.Tripakis. Type Inference of Simulink Hierarchical Block Diagrams in Isabelle. FORTE 2017
    [paper]  [technical report]  [slides]
  4. V. Preoteasa, I. Dragomir, S.Tripakis. A Nondeterministic and Abstract Algorithm for Translating Hierarchical Block Diagrams. arXiv 2016
    [technical report]
  5. V. Preoteasa, S.Tripakis. Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. LICS 2016
    [paper]  [technical report]
  6. S.Tripakis. Compositionality in the Science of System Design. Proceedings of the IEEE 2016
    [paper]
  7. I. Dragomir, V. Preoteasa, S.Tripakis. Compositional Semantics and Analysis of Hierarchical Block Diagrams. SPIN 2016
    [paper]  [technical report]  [slides]
  8. V. Preoteasa, S.Tripakis. Refinement Calculus of Reactive Systems. EMSOFT 2014
    [paper]  [technical report]
  9. V. Preoteasa. Formalization of Refinement Calculus for Reactive Systems. Archive of Formal Proofs 2014
    [paper]  [source]
  10. S. Tripakis, C. Stergiou, M. Broy, E. A. Lee. Error-Completion in Interface Theories. SPIN 2013
    [paper]
  11. S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. A Theory of Synchronous Relational Interfaces. ACM TOPLAS 2011
    [paper]
  12. 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.