计算机时代
計算機時代
계산궤시대
COMPUTER ERA
2011年
6期
1-3
,共3页
吴永刚%陆慧娟%程倬%陈江
吳永剛%陸慧娟%程倬%陳江
오영강%륙혜연%정탁%진강
时间自动机%实时系统%UPPAAL%模型验证
時間自動機%實時繫統%UPPAAL%模型驗證
시간자동궤%실시계통%UPPAAL%모형험증
实时系统必须在一个事先定义好的时间限制内对来自外部或内部的事件进行响应,如何有效验证实时模型的正确性和安全性是一个难点.文章通过多个时间自动机来模拟实时系统中的各个对象,并用UPPAAL对模型进行验证,减少了模型验证的状态搜索空间,为实时嵌入式系统开发和验证提供了一种可行、安全的控制机制.实验结果显示了系统的有效性.
實時繫統必鬚在一箇事先定義好的時間限製內對來自外部或內部的事件進行響應,如何有效驗證實時模型的正確性和安全性是一箇難點.文章通過多箇時間自動機來模擬實時繫統中的各箇對象,併用UPPAAL對模型進行驗證,減少瞭模型驗證的狀態搜索空間,為實時嵌入式繫統開髮和驗證提供瞭一種可行、安全的控製機製.實驗結果顯示瞭繫統的有效性.
실시계통필수재일개사선정의호적시간한제내대래자외부혹내부적사건진행향응,여하유효험증실시모형적정학성화안전성시일개난점.문장통과다개시간자동궤래모의실시계통중적각개대상,병용UPPAAL대모형진행험증,감소료모형험증적상태수색공간,위실시감입식계통개발화험증제공료일충가행、안전적공제궤제.실험결과현시료계통적유효성.
