The Refinement Calculus of Reactive Systems Toolset - Feb 2018

Distribution of the Refinement Calculus of Reactive Systems (RCRS) Toolset. Includes full RCRS formalization in the Isabelle proof assistant, Formal Analyzer implemented on top of Isabelle, Translator of Simulink models to RCRS, sample Simulink models, and demonstration files with instructions.<br>RCRS is fully implemented in the Isabelle theorem prover. The RCRS implementation currently consists of 22 Isabelle theories (.thy files).<br>This dataset is in .zip archive format and can be uncompressed using standard compression software. This dataset consists of:<br><b>- instructions-figshare.txt - </b>Step-by-step instructions on how to use this artifact to replicate the results in the TACAS 2018 paper: "The Refinement Calculus of Reactive Systems Toolset" in openly accessible .txt format.<b>- RCRS_Demo.thy - </b>a demo file for RCRS in openly-accessible Isabelle <b>.thy</b> format. <b>- Documentation/ - </b>guidance documents in openly accessible <b>.pdf </b>format on RCRS and a theory dependency graph.<b>- RCRS/ - </b>data are in either openly-accessible Python language <b>.py</b> format or Isabelle theorem <b>.thy</b> format. RCRS contains two subfolders: I. The "Isabelle" folder contains the implementation of RCRS into the Isabelle proof assistant. See file "document.pdf" for documentation on the subfolders. II. The "Simulink2Isabelle" folder contains the "simulink2isabelle.py" translator: it translates Simulink models into RCRS/Isabelle theories.<br><b>- Simulink_models/ </b> - data are in <b>.slx</b> format, accessible via MathWorks Matlab/Simulink. These form the Translator inputs.<br>The instructions allow to reproduce in full the results reported in the paper "The Refinement Calculus of Reactive Systems Toolset", TACAS 2018.<br>