Verification of real-time systems by abstraction of time constraints
Verification of real-time systems by abstraction of time constraints
复制标题
通过抽象时间约束来验证实时系统
DOI：
10.1109/ipdps.2003.1213432
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
M. Benmohamed
中科院分区：
文献类型：
--
作者：
M. Bourahla;M. Benmohamed
提出了一种基于时间谓词抽象的实时系统模型检测方法。一个实时系统的建模与时间自动机被翻译成一个实时程序。这些属性是用时态逻辑TCTL（时间计算树逻辑）来指定的。首先使用的实时程序和TCTL属性，用于产生一个新的自动机，该自动机增加了原来的辅助时钟捕获的定时约束的TCTL规范，减少到一个等效的CTL规范。第二，增强的实时程序被转换成一个良好的定时系统，通过删除zeno运行（即时间不发散的执行）。然后，在增广自动机的时间谓词表示的增广和无zeno实时程序将被抽象，以产生一个untimed自动机表示一个等价的有限状态系统的模型检查使用现有的工具。
This paper presents a new methodology for model checking real-time systems based on the abstraction of time predicates. A real-time system is modeled with a timed automaton which is translated to a real-time program. The properties are specified with the temporal logic TCTL (timed computational tree logic). The real-time program and the TCTL property are used first, for producing a new automaton which augments the original with auxiliary clocks capturing the timing constraints in the TCTL specification that is reduced to an equivalent CTL specification. Second, the augmented real-time program is converted to a well timed system by removing the zeno runs (that are executions in which time does not diverge). Then the time predicates in the augmented automaton which is represented by an augmented and no-zeno real-time program will be abstracted to generate an untimed automaton representing an equivalent finite state system to be model checked using existing tools.