论文研究-一种基于有限精度时间自动机的模型检测工具.pdf

收稿日期: 2005-05-09; 修返日期: 2006-02-17

基金 项 目: 国 家 自 然 科 学 基 金 资 助 项 目 ( 60273025) ; 国 家

“973”计划资助项目( 2002CB312200)

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

*

徐雨波

1, 2

, 晏荣杰

1

( 1. 中国 科学 院 软 件研 究所 计 算机 科学 国家 重点 实验室 , 北 京 100080; 2. 中 国科 学院 研究 生院 , 北京 100049)

摘 要: 基 于有 限精 度时 间自 动机 模型 , 实 现了 一种 新 的数 据 结 构———SDS , 用 SDS 符号 化 表 示状 态 空 间 的 实

( 1. Key Lab. for Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China; 2. Graduate School, Chinese

Academy of Sciences, Beijing 100049, China)

Abstract: Based on the theoryof Finite Precision Timed Automata( FPTA) , this article implements a kind of datastructure,

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 perfor-

mance of the tool is good in most cases.

Key words: Model-checking Tool; Real-time Systems; Data Structure; Finite Precision; Timed Automata

实时系统应用领域诸如航天航空控制系统、核反应堆控制

系统、实时通信系统等, 对系统的安全性、可靠性和正确性都提

出了很高的要求, 尤 其 在一 些高 尖 端领 域比 如 航空 航天 领 域

只能发现系统或者程序中的 部分错 误, 并且需 要手动 完成; 而

模型检测方法是通过对程序状态空间的穷尽搜索, 针对某一个

特性发现系统或者程序中的 错误, 并且 可以自 动完成, 无须 人

法, 完成程序的自动验证, 目前 存在许 多基于 不同逻 辑理论 的

方法和工具来验证有穷状态系统。对于非实时系统, 其模型检

测的理论和工具的研究比较成熟, 目前比较著名 的是基于 LTL

的模型检测工具 SPIN

和基于 CTL 的模型检测工具 SMV

[ 4]

[ 5]

工具是针对实时反应型系统的模型检测工具, 其理论基础是有

限精度时 间 自 动机 ( Finite Precision Timed Automata, FPTA) 。

FPTAT工具根据自身的语 义特点 实现了 相应的 数据结 构———

间, 实现了基于深度优先搜索和广度优先搜索两种模型检测算

动机的一种变形, 其 中“有 限精 度”主要 体现 在时 钟变 量的 定

义和状态迁移的语义定义上, 这一 节主要 介绍时 间自动 机, 有

1. 1 时间自动机

有满足转移边上的卫条 件( Guard ) 才 可以从 一个 节点 转移 到

: : =x ～d| |

1

2

. ～∈{ < , ≤, > , ≥ }