计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2013年
5期
318-321
,共4页
综合性能%形式化验证%马尔可夫过程%时序逻辑%自动机%积模型
綜閤性能%形式化驗證%馬爾可伕過程%時序邏輯%自動機%積模型
종합성능%형식화험증%마이가부과정%시서라집%자동궤%적모형
integrated performance%formal verification%Markov process%temporal logic%automata%product model
面向复杂信息系统综合性能的形式化验证问题,以数据传输系统为例,使用一种基于改进的马尔可夫判定过程验证分析方法进行复杂信息系统的性能验证.在综合各种连续随机逻辑变体基础上,采用一种表达能力更强的时序逻辑来表示系统模型的复杂性质,运用自动机技术建模路径公式,通过构造积模型完成模型与自动机的同步演化,并给出相应的算法描述.实例结果验证了该方法可有效地扩大模型检测技术的应用范围.
麵嚮複雜信息繫統綜閤性能的形式化驗證問題,以數據傳輸繫統為例,使用一種基于改進的馬爾可伕判定過程驗證分析方法進行複雜信息繫統的性能驗證.在綜閤各種連續隨機邏輯變體基礎上,採用一種錶達能力更彊的時序邏輯來錶示繫統模型的複雜性質,運用自動機技術建模路徑公式,通過構造積模型完成模型與自動機的同步縯化,併給齣相應的算法描述.實例結果驗證瞭該方法可有效地擴大模型檢測技術的應用範圍.
면향복잡신식계통종합성능적형식화험증문제,이수거전수계통위례,사용일충기우개진적마이가부판정과정험증분석방법진행복잡신식계통적성능험증.재종합각충련속수궤라집변체기출상,채용일충표체능력경강적시서라집래표시계통모형적복잡성질,운용자동궤기술건모로경공식,통과구조적모형완성모형여자동궤적동보연화,병급출상응적산법묘술.실례결과험증료해방법가유효지확대모형검측기술적응용범위.