Real-Time Verification of Statemate Designs
Real-Time Verification of Statemate Designs
复制标题
Statemate 设计的实时验证
DOI：
10.1007/bfb0028777
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
Gunnar Wittich
中科院分区：
文献类型：
--
作者：
Udo Brockmeyer;Gunnar Wittich
本文提出了一个用于状态设计实时验证的工具集。Statemate是一种广泛应用于嵌入式控制应用的设计工具。在该方法中，包含所有时序信息的设计被转换为非定时有限状态机(FSM)，并通过符号模型检测进行验证。实时要求通过在离散时间上解释的TCTL公式来表示。实现了从TCTL模型检测到CTL模型检测的简化，以便使用CTL模型检查器来完成验证任务。给出了该工具集的部分实验结果。
This paper presents a toolset for real-time verification of Statemate designs. Statemate is a widely used design tool for embedded control applications. In our approach designs including all timing information are translated into untimed finite state machines (FSMs) which are verified by symbolic model-checking. Real-time requirements are expressed by TCTL formulae interpreted over discrete time. A reduction from TCTL model-checking to CTL model-checking is implemented in order to use a CTL model-checker for the verification task. Some experimental results of the toolset are given.