计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2006年
6期
1-6,100
,共7页
陈铭松%赵建华%李宣东%郑国梁
陳銘鬆%趙建華%李宣東%鄭國樑
진명송%조건화%리선동%정국량
实时系统%时间自动机%状态空间爆炸%可达性分析
實時繫統%時間自動機%狀態空間爆炸%可達性分析
실시계통%시간자동궤%상태공간폭작%가체성분석
时间自动机是检验实时系统建模的有效工具,其可达性分析可以检验系统是否可能达到某些特定的状态,其算法通常采用对符号状态的枚举来遍历其状态空间.因为引入了时钟变量,时间自动机的可达性分析算法会产生大量的中间状态,需要巨大的存储空间,往往超出了计算机能力的极限,导致分析和检验不能完成.这就是所谓的"状态空间爆炸".研究人员设计了很多种优化技术来约减可达性分析所需的存储空间,以解决或者缓解这个问题.本文首先介绍了时间自动机及其可达性分析的基本概念,然后分类讨论了现有的空间约减优化技术并对此做出总结,最后提出了一些未来的研究方向.
時間自動機是檢驗實時繫統建模的有效工具,其可達性分析可以檢驗繫統是否可能達到某些特定的狀態,其算法通常採用對符號狀態的枚舉來遍歷其狀態空間.因為引入瞭時鐘變量,時間自動機的可達性分析算法會產生大量的中間狀態,需要巨大的存儲空間,往往超齣瞭計算機能力的極限,導緻分析和檢驗不能完成.這就是所謂的"狀態空間爆炸".研究人員設計瞭很多種優化技術來約減可達性分析所需的存儲空間,以解決或者緩解這箇問題.本文首先介紹瞭時間自動機及其可達性分析的基本概唸,然後分類討論瞭現有的空間約減優化技術併對此做齣總結,最後提齣瞭一些未來的研究方嚮.
시간자동궤시검험실시계통건모적유효공구,기가체성분석가이검험계통시부가능체도모사특정적상태,기산법통상채용대부호상태적매거래편력기상태공간.인위인입료시종변량,시간자동궤적가체성분석산법회산생대량적중간상태,수요거대적존저공간,왕왕초출료계산궤능력적겁한,도치분석화검험불능완성.저취시소위적"상태공간폭작".연구인원설계료흔다충우화기술래약감가체성분석소수적존저공간,이해결혹자완해저개문제.본문수선개소료시간자동궤급기가체성분석적기본개념,연후분류토론료현유적공간약감우화기술병대차주출총결,최후제출료일사미래적연구방향.
