Analysis of Real-Time Systems with CTL Model Checkers
Analysis of Real-Time Systems with CTL Model Checkers
复制标题
使用 CTL 模型检查器分析实时系统
DOI：
10.1016/j.entcs.2004.08.057
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
M. Benmohamed
中科院分区：
文献类型：
--
作者：
M. Bourahla;M. Benmohamed
提出了一种新的稠密实时系统模型检测方法。用时间自动机对稠密实时系统进行建模，并用时序逻辑TCTL描述其性质。TCTL属性的描述被简化为CTL，它的时间约束被捕获在一个新的时间自动机中。该时间自动机将与指定被分析的实时系统的原始时间自动机组成。然后，利用基于强互模拟的状态空间划分求精方法对产品定时自动机进行抽象。其结果是一个以TCTL属性为模的无时间自动机，它表示一个等价的有限状态系统，该系统将使用现有的CTL模型检测工具进行模型检测。
This paper presents a new method for model checking dense real-time systems. The dense real-time system is modeled by a timed automaton and the property is specified with the temporal logic TCTL. Specification of the TCTL property is reduced to CTL and its temporal constraints are captured in a new timed automaton. This timed automaton will be composed with the original timed automaton specifying the real-time system under analysis. Then, the product timed au- tomaton will be abstracted using partition refinement of state space based on strong bi-simulation. The result is an untimed automaton modulo the TCTL property which represents an equivalent finite state system to be model checked using existing CTL model checking tools.