RCRS

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.