The Refinement Calculus of Reactive Systems
The Refinement Calculus of Reactive Systems
复制标题
DOI：
10.1016/j.ic.2021.104819
复制
发表时间：
2017-10
期刊：
影响因子：
--
通讯作者：
V. Preoteasa;I. Dragomir;S. Tripakis
中科院分区：
文献类型：
--
作者：
V. Preoteasa;I. Dragomir;S. Tripakis
Refinement Calculus of Reactive Systems（RCRS）是一个用于反应式系统建模和推理的组合形式化框架。RCRS提供了一种语言，它可以描述原子组件作为符号转换系统或QTL公式，和复合组件形成使用三个原始的组合操作符：串行，并行和反馈。该语言的语义给出的单调属性变换器，单调谓词变换器的反应系统的扩展。RCRS可以指定安全性和活性属性。它还可以对既不确定又不接受输入的输入-输出系统进行建模（即，其可以在某些时间点拒绝某些输入），并且因此可以被视为行为类型系统。RCRS提供了一套符号计算机辅助推理的技术，包括组合静态分析和验证。RCRS附带了一个公开的实现，其中包括在Isabelle证明助手中对RCRS理论的完整形式化。
The Refinement Calculus of Reactive Systems (RCRS) is a compositional formal framework for modeling and reasoning about reactive systems. RCRS provides a language which can describe atomic components as symbolic transition systems or QLTL formulas, and composite components formed using three primitive composition operators: serial, parallel, and feedback. The semantics of the language is given in terms of monotonic property transformers, an extension of monotonic predicate transformers to reactive systems. RCRS can specify both safety and liveness properties. It can also model input-output systems which are both non-deterministic and non-input-receptive (i.e., which may reject some inputs at some points in time), and can thus be seen as a behavioral type system. RCRS provides a set of techniques for symbolic computer-aided reasoning, including compositional static analysis and verification. RCRS comes with a publicly available implementation which includes a complete formalization of the RCRS theory in the Isabelle proof assistant.