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:


  1. V. Preoteasa, I. Dragomir, S.Tripakis. Type Inference of Simulink Hierarchical Block Diagrams in Isabelle. arXiv, 2016
  2. V. Preoteasa, I. Dragomir, S.Tripakis. A Nondeterministic and Abstract Algorithm for Translating Hierarchical Block Diagrams. arXiv, 2016
  3. V. Preoteasa, S.Tripakis. Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. LICS 2016
    [paper]  [technical report]
  4. I. Dragomir, V. Preoteasa, S.Tripakis. Compositional Semantics and Analysis of Hierarchical Block Diagrams. SPIN 2016
    [paper]  [technical report]  [slides]
  5. V. Preoteasa, S.Tripakis. Refinement Calculus of Reactive Systems. EMSOFT 2014
    [paper]  [technical report]
  6. V. Preoteasa. Formalization of Refinement Calculus for Reactive Systems. Archive of Formal Proofs 2014
    [paper]  [source]
  7. S. Tripakis, C. Stergiou, M. Broy, E. A. Lee. Error-Completion in Interface Theories. SPIN 2013
  8. S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. A Theory of Synchronous Relational Interfaces. ACM TOPLAS 2011
  9. S. Tripakis, B. Lickly, T. A. Henzinger, E. A. Lee. On Relational Interfaces. EMSOFT 2009


For any enquiries, you can contact us by email.