主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
晏荣杰,李广元,徐雨波,刘春明,唐稚松.有限精度时间自动机的可达性检测.软件学报,2006,17(1):1-10
有限精度时间自动机的可达性检测
Reachability Checking of Finite Precision Timed Automata
投稿时间:2004-04-28  修订日期:2005-07-11
DOI:
中文关键词:  有限精度时间自动机  符号化方法  模型检测  可达性
英文关键词:finite precision timed automata  symbolic method  model checking  reachability
基金项目:the National Natural Science Foundation of China under Grant Nos.60273025, 60223005, 60421001 (国家自然科学基金); the National Grand Fundamental Research 973 Program of China under Grant No.2002cb312200 (国家重点基础研究发展规划(973))
作者单位
晏荣杰 中国科学院 软件研究所 计算机科学重点实验室,北京 100080
中国科学院 研究生院,北京 100049 
李广元 中国科学院 软件研究所 计算机科学重点实验室,北京 100080 
徐雨波 中国科学院 软件研究所 计算机科学重点实验室,北京 100080
中国科学院 研究生院,北京 100049 
刘春明 中国科学院 软件研究所 计算机科学重点实验室,北京 100080
中国科学院 研究生院,北京 100049 
唐稚松 中国科学院 软件研究所 计算机科学重点实验室,北京 100080 
摘要点击次数: 3607
全文下载次数: 3013
中文摘要:
      为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finite precision timed automata,简称FPTA)作为实时系统的形式模型,并提出了一种数据结构SDS(series of delay sequence)符号化表示状态空间中的状态集.FPTA只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,Alur与Dill提出的时间自动机的可达性检测可简化为FPTA的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了SDS的特点及不足.
英文摘要:
      To relieve the state space explosion problem, and accelerate the speed of model checking, this paper introduces the concept of finite precision timed automata (FPTAs) and proposes a data structure to represent its symbolic states. FPTAs only record the integer values of clock variables together with the order of their most recent resets to reduce the state space. The constraints under which the reachability checking of a timed automaton can be reduced to that of the corresponding FPTA are provided, and then an algorithm for reachability analysis is presented. Finally, the paper presents some preliminary experimental results, and analyzes the advantages and disadvantages of the new data structure.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利