Refinement Calculus of Reactive Systems

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


Implementation and download


Our group is developing a publicly available implementation of RCRS. The distribution currently includes: 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:

Papers


  1. I. Dragomir, V. Preoteasa, S.Tripakis. The Refinement Calculus of Reactive Systems Toolset. arXiv 2017
    [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.