The Refinement Calculus of Reactive Systems Toolset
The Refinement Calculus of Reactive Systems Toolset
复制标题
DOI：
10.1007/s10009-020-00561-4
复制
发表时间：
2017-10
影响因子：
1.5
通讯作者：
I. Dragomir;V. Preoteasa;S. Tripakis
中科院分区：
文献类型：
--
作者：
I. Dragomir;V. Preoteasa;S. Tripakis
我们介绍了反应系统工具集的细化演算，这是一个关于反应系统的组合形式化建模和推理的环境，围绕Isabelle、Simulink和Python构建。该工具集实现了反应系统的细化演算（RCRS），这是一个基于契约的细化框架，灵感来自经典的细化演算和接口理论。该工具集在大约30000行Isabelle代码中形式化了整个RCRS理论。该工具集还包含一个Simulink图的翻译器和一个在Isabelle之上实现的形式化分析器。我们通过一系列教学实例介绍了RCRS工具集的主要功能，并描述了一个来自汽车领域的更大的案例研究。
We present the Refinement Calculus of Reactive Systems Toolset, an environment for compositional formal modeling and reasoning about reactive systems, built around Isabelle, Simulink, and Python. The toolset implements the Refinement Calculus of Reactive Systems (RCRS), a contract-based refinement framework inspired by the classic refinement calculus and interface theories. The toolset formalizes the entire RCRS theory in about 30000 lines of Isabelle code. The toolset also contains a translator of Simulink diagrams and a formal analyzer implemented on top of Isabelle. We present the main functionalities of the RCRS Toolset via a series of pedagogical examples and also describe a larger case study from the automotive domain.