软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2006年
1期
1-10
,共10页
晏荣杰%李广元%徐雨波%刘春明%唐稚松
晏榮傑%李廣元%徐雨波%劉春明%唐稚鬆
안영걸%리엄원%서우파%류춘명%당치송
有限精度时间自动机%符号化方法%模型检测%可达性
有限精度時間自動機%符號化方法%模型檢測%可達性
유한정도시간자동궤%부호화방법%모형검측%가체성
为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finite precision timed automata,简称FPTA)作为实时系统的形式模型,并提出了一种数据结构SDS(series ofdelay sequence)符号化表示状态空间中的状态集.FPTA只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,Alur与Dill提出的时间自动机的可达性检测可简化为FPTA的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了SDS的特点及不足.
為瞭緩解狀態空間爆炸問題,減小模型檢測過程中生成的狀態空間,加快模型檢測速度,引入有限精度時間自動機(finite precision timed automata,簡稱FPTA)作為實時繫統的形式模型,併提齣瞭一種數據結構SDS(series ofdelay sequence)符號化錶示狀態空間中的狀態集.FPTA隻記錄時鐘變量的整數值及時鐘變化的先後次序,從而減小生成的狀態空間.在一定的時間約束下,Alur與Dill提齣的時間自動機的可達性檢測可簡化為FPTA的可達性檢測.舉例描述瞭狀態空間的生成過程和錶示方法.最後,列齣部分初步的實驗結果,分析瞭SDS的特點及不足.
위료완해상태공간폭작문제,감소모형검측과정중생성적상태공간,가쾌모형검측속도,인입유한정도시간자동궤(finite precision timed automata,간칭FPTA)작위실시계통적형식모형,병제출료일충수거결구SDS(series ofdelay sequence)부호화표시상태공간중적상태집.FPTA지기록시종변량적정수치급시종변화적선후차서,종이감소생성적상태공간.재일정적시간약속하,Alur여Dill제출적시간자동궤적가체성검측가간화위FPTA적가체성검측.거례묘술료상태공간적생성과정화표시방법.최후,렬출부분초보적실험결과,분석료SDS적특점급불족.
