一种基于有限精度时间自动机的模型检测工具

Model-checking Tool Based on Finite Precision Timed Automata (FPTA)

基于有限精度时间自动机模型,实现了一种新的数据结构———SDS,用SDS符号化表示状态空间的实时系统模型检测工具,并进行了初步的实验分析,取得了良好的效果。

Based on the theory of Finite Precision Timed Automata （FPTA）, this article implements a kind of data structure, named series of delay sequence （SDS） , to describe the state space symbolically. Then implement a model-checking tool for real-time systems based on the data structure of SDS. From primary experiment results, it can be concluded that the performance of the tool is good in most cases.