Automatic Symbolic Veri cation of Embedded Systems
Automatic Symbolic Veri cation of Embedded Systems
复制标题
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
T. Henzinger;Pei-Hsin Ho
中科院分区：
文献类型：
--
作者：
T. Henzinger;Pei-Hsin Ho
我们提出了一种用于嵌入式系统自动验证的模型检查程序及其实现。该系统组件被描述为具有有限控制和代表连续环境参数（例如时间、压力和温度）的实值变量的混合自动机|通信机器。系统要求在带有秒表的时间逻辑中指定，并通过符号 xpoint 计算进行验证。康奈尔混合技术工具 HyTech 中实施的验证过程适用于混合自动机，其连续动态由变量及其导数的线性约束控制。我们通过检查数字控制器、调度器和分布式算法的安全性、活跃性、时间限制和持续时间要求来说明该方法和工具。
We present a model-checking procedure and its implementation for the automatic veri cation of embedded systems. The system components are described as Hybrid Automata|communicating machines with nite control and real-valued variables that represent continuous environment parameters such as time, pressure, and temperature. The system requirements are speci ed in a temporal logic with stop watches, and veri ed by symbolic xpoint computation. The veri cation procedure|implemented in the Cornell Hybrid Technology Tool, HyTech|applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded, and duration requirements of digital controllers, schedulers, and distributed algorithms.