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: serial, parallel, 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.