-
题名有限精度时间自动机的可达性检测
被引量:5
- 1
-
-
作者
晏荣杰
李广元
徐雨波
刘春明
唐稚松
-
机构
中国科学院软件研究所计算机科学重点实验室
-
出处
《软件学报》
EI
CSCD
北大核心
2006年第1期1-10,共10页
-
基金
国家自然科学基金
国家重点基础研究发展规划(973)~~
-
文摘
为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finite precision timed automata,简称FPTA)作为实时系统的形式模型,并提出了一种数据结构SDS(series of delay sequence)符号化表示状态空间中的状态集.FPTA只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,Alur与Dill提出的时间自动机的可达性检测可简化为FPTA的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了SDS的特点及不足.
-
关键词
有限精度时间自动机
符号化方法
模型检测
可达性
-
Keywords
finite precision timed automata
symbolic method
model checking
reachability
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名一种基于有限精度时间自动机的模型检测工具
被引量:1
- 2
-
-
作者
徐雨波
晏荣杰
-
机构
中国科学院软件研究所计算机科学国家重点实验室
-
出处
《计算机应用研究》
CSCD
北大核心
2006年第5期121-125,共5页
-
基金
国家自然科学基金资助项目(60273025)
国家"973"计划资助项目(2002CB312200)
-
文摘
基于有限精度时间自动机模型,实现了一种新的数据结构———SDS,用SDS符号化表示状态空间的实时系统模型检测工具,并进行了初步的实验分析,取得了良好的效果。
-
关键词
模型检测工具
实时系统
数据结构
有限精度
时间自动机
-
Keywords
Model-checking Tool
Real-time Systems
Data Structure
Finite Precision
Timed Automata
-
分类号
TP316
[自动化与计算机技术—计算机软件与理论]
-
-
题名有限精度时间自动机的时钟表示
- 3
-
-
作者
刘春明
晏荣杰
徐雨波
-
机构
中国科学院软件研究所计算机科学重点实验室
-
出处
《计算机应用研究》
CSCD
北大核心
2006年第7期23-25,31,共4页
-
基金
国家自然科学基金资助项目(60273025
60223005
+1 种基金
60421001)
国家"973"计划资助项目(2002cb312200)
-
文摘
简要介绍了有限精度时间自动机(FPTA)的基本概念,重点讨论FPTA状态中时钟的表示。FPTA只记录时钟值的整数部分,而用时钟序的概念来模拟表示时钟值小数部分的大小关系,从而减少生成的状态空间。在FPTA模型中,时钟操作的时空性能主要依赖于时钟序的数据结构和算法。提出了用位矩阵来表示时钟序的数据结构POM(Partial-OrderMatrix)。采用该结构的操作算法具有O(n)复杂度,且无需标准化操作;同时,一切操作均可以通过位运算实现,从而大幅度提高时钟操作的时间效率。
-
关键词
有限精度时间自动机
模型检验
符号化方法
-
Keywords
Finite Precision Timed Automata(FFFA)
Model Checking
Symbolic Methods
-
分类号
TP301.1
[自动化与计算机技术—计算机系统结构]
-