| 一种改进的实时系统可达性分析算法 |
| |
| 引用本文： | 岳香芬,缪淮扣,许庆国.一种改进的实时系统可达性分析算法[J].上海大学学报(自然科学版),2006,12(3):311-315. |
| |
| 作者姓名： | 岳香芬 缪淮扣 许庆国 |
| |
| 作者单位： | 上海大学,计算机工程与科学学院,上海,200072 |
| |
| 基金项目： | 国家自然科学基金;上海市教委资助项目 |
| |
| 摘 要： | 首先简介了时间自动机、时钟区域、区域等价、时钟带的概念.利用时钟带,可以将时间自动机的无穷状态空间转化为有穷.实时系统的绝大多数安全性和部分活性可以通过可达性分析算法来验证.然而,当系统时钟个数较多时,用DBM存储时钟带,会造成内存空间的很大耗费.该文提出了用邻接表存储时钟带,给出了改进的算法,并对算法的空间复杂度作了分析.实验表明,当时钟个数大于5时能节约很大的内存空间,从而在一定程度上缓解了状态爆炸.
|
| 关 键 词： | 模型检查 时间自动机 时钟带 可达性分析 |
| 文章编号： | 1007-2861（2006）03-0311-05 |
| 收稿时间： | 2005-09-05 |
| 修稿时间： | 2005年9月5日 |
Improvement to a Reachability Analysis Algorithm for Real-Time Systems |
| |
| YUE Xiang-fen,MIAO Huai-kou,XU Qing-guo.Improvement to a Reachability Analysis Algorithm for Real-Time Systems[J].Journal of Shanghai University(Natural Science),2006,12(3):311-315. |
| |
| Authors: | YUE Xiang-fen MIAO Huai-kou XU Qing-guo |
| |
| Affiliation: | School of Computer Engineering and Science, Shanghai University, Shanghai 200072, China |
| |
| Abstract: | This paper first briefly introduces timed automata,clock region,region equivalence and clock zone.According to clock zone,infinite state space of timed automata can be transformed to finite.For most safety properties and some liveness properties,model checking can be reduced to reachability analysis.However,when the number of clocks is large,using DBM to store clock zone may cause large memory requirements.In view of this,the paper proposes an improved algorithm that uses AdjLink to store clock zone,and analyzes its space complexity.Experiments show that when the number of clocks is greater than 5,this method can save much memory therefore relieve the state-space explosion to some extent. |
| |
| Keywords: | model checking timed automata clock zone reachability analysis |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
