SimCheck: a contract type system for Simulink
SimCheck: a contract type system for Simulink
复制标题
SimCheck：Simulink 的合约类型系统
DOI：
--
复制
发表时间：
2011
影响因子：
1.2
通讯作者：
N. Shankar
中科院分区：
文献类型：
--
作者：
Pritam Roy;N. Shankar
Matlab Simulink™是一类用于建模和仿真物理和网络物理系统的可视化语言的成员。Simulink模型由输入和输出端口通过传输信号的链路连接的模块组成。我们提供了一个基于合同的类型系统的Simulink与注释和尺寸/单位与端口和链接。这些合约类型可以捕获信号上的不变量以及信号之间的关系。我们定义了一个基于合同的验证器，检查这些合同的Simulink块的良好形成。该验证器生成由SRI的Yices求解器解决的可满足性模理论（SMT）的证明义务。这种转换可以用来检测基本类型错误和违反契约，演示反例，生成测试用例，或证明不存在基于契约的类型错误。我们的工作是符号分析的Matlab Simulink模型的第一步。
Matlab Simulink™ is a member of a class of visual languages that are used for modeling and simulating physical and cyber-physical system. A Simulink model consists of blocks with input and output ports connected using links that carry signals. We provide a contract-based type system of Simulink with annotations and dimensions/units associated with ports and links. These contract types can capture invariants on signals as well as relations between signals. We define a contract-based verifier that checks the well formedness of Simulink blocks with respect to these contracts. This verifier generates proof obligations that are solved by SRI’s Yices solver for satisfiability modulo theories (SMT). This translation can be used to detect basic type errors and violation of contracts, demonstrate counterexamples, generate test cases, or prove the absence of contract-based type errors. Our work is an initial step toward the symbolic analysis of Matlab Simulink models.