火力与指挥控制
火力與指揮控製
화력여지휘공제
FIRE CONTROL & COMMAND CONTROL
2011年
12期
134-137
,共4页
形式化验证%模型检验%Petri网%时间自动机
形式化驗證%模型檢驗%Petri網%時間自動機
형식화험증%모형검험%Petri망%시간자동궤
日益复杂的军事电子信息系统面临正确性验证挑战,形式化验证方法如模型检验技术成为必需.给出基于时间Petri网表示的军事电子系统模型PMES的定义,然后给出PMES模型转换为时间自动机网的步骤,利用已有的基于时间自动机的模型检验工具对系统性质进行验证;系统的性质要求用时序逻辑语言CTL或TCTL公式表示.雷达干扰机系统说明了该方法的实际应用效果.
日益複雜的軍事電子信息繫統麵臨正確性驗證挑戰,形式化驗證方法如模型檢驗技術成為必需.給齣基于時間Petri網錶示的軍事電子繫統模型PMES的定義,然後給齣PMES模型轉換為時間自動機網的步驟,利用已有的基于時間自動機的模型檢驗工具對繫統性質進行驗證;繫統的性質要求用時序邏輯語言CTL或TCTL公式錶示.雷達榦擾機繫統說明瞭該方法的實際應用效果.
일익복잡적군사전자신식계통면림정학성험증도전,형식화험증방법여모형검험기술성위필수.급출기우시간Petri망표시적군사전자계통모형PMES적정의,연후급출PMES모형전환위시간자동궤망적보취,이용이유적기우시간자동궤적모형검험공구대계통성질진행험증;계통적성질요구용시서라집어언CTL혹TCTL공식표시.뢰체간우궤계통설명료해방법적실제응용효과.
