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

  • 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: serialparallel, 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.
License: 
MIT
Provider: 
SPACE SYSTEMS FINLAND OY
Keywords: 
Simulation
Formal methods
Testing
Verification
Checking Compatibility
main contact: 
Viorel Preoteasa

Downloads

RCRS tool can be downloaded from the RCRS site (see link below)

Documentation

RCRS tool documentation is available at the RCRS site (see link below)

Source Code

RCRS tool source code is available at the RCRS site (see link below)