计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2013年
4期
58-64,76
,共8页
线性混成自动机%迁移系统%安全性验证%不变式生成
線性混成自動機%遷移繫統%安全性驗證%不變式生成
선성혼성자동궤%천이계통%안전성험증%불변식생성
混成自动机行为中既包含离散行为又包含连续行为,非常复杂.其安全性验证问题难以解决,即使是线性混成自动机,它的可达性问题也被证明是不可判定的.现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集,复杂度高,可处理问题规模非常有限.为了避免这类问题,实现了一种新的工具.该工具将线性混成自动机表达为等价的迁移系统,并利用迁移系统上不变式生成相关工作对混成自动机进行验证.实验数据表明,方法有效可行,工具具有良好的性能.
混成自動機行為中既包含離散行為又包含連續行為,非常複雜.其安全性驗證問題難以解決,即使是線性混成自動機,它的可達性問題也被證明是不可判定的.現有工具大都使用多麵體計算來計算線性混成自動機的可達狀態空間集,複雜度高,可處理問題規模非常有限.為瞭避免這類問題,實現瞭一種新的工具.該工具將線性混成自動機錶達為等價的遷移繫統,併利用遷移繫統上不變式生成相關工作對混成自動機進行驗證.實驗數據錶明,方法有效可行,工具具有良好的性能.
혼성자동궤행위중기포함리산행위우포함련속행위,비상복잡.기안전성험증문제난이해결,즉사시선성혼성자동궤,타적가체성문제야피증명시불가판정적.현유공구대도사용다면체계산래계산선성혼성자동궤적가체상태공간집,복잡도고,가처리문제규모비상유한.위료피면저류문제,실현료일충신적공구.해공구장선성혼성자동궤표체위등개적천이계통,병이용천이계통상불변식생성상관공작대혼성자동궤진행험증.실험수거표명,방법유효가행,공구구유량호적성능.
