系统工程与电子技术
繫統工程與電子技術
계통공정여전자기술
SYSTEMS ENGINEERING AND ELECTRONICS
2011年
2期
458-463
,共6页
李震%刘斌%李小勋%殷永峰
李震%劉斌%李小勛%慇永峰
리진%류빈%리소훈%은영봉
软件工程%Petri网%模型检验%安全关键软件%形式化方法
軟件工程%Petri網%模型檢驗%安全關鍵軟件%形式化方法
연건공정%Petri망%모형검험%안전관건연건%형식화방법
需求形式化建模和模型检验可以提高安全关健软件的可信性,但在模型描述、调试和解释能力方面存在局限.对使用Petri网支持软件系统建模进行了扩展,设定默认值为零的权函数、利用"非"虚线描述在状态为假和变迁失败情况下的触发,增强阈值条件的描述能力,区分了枚举型和数值型库所,区分了普通迁移和强赋值迁移,并给出了扩展后的形式化定义及其和检验语言的语义映射.最后给出在典型机载软件上的应用,建立了软件需求模型和部分映射代码,对模型进行检验、反例路径分析和需求完善.过程和结果表明该方法可以有效的支持实际的关键安全软件需求建模和验证.
需求形式化建模和模型檢驗可以提高安全關健軟件的可信性,但在模型描述、調試和解釋能力方麵存在跼限.對使用Petri網支持軟件繫統建模進行瞭擴展,設定默認值為零的權函數、利用"非"虛線描述在狀態為假和變遷失敗情況下的觸髮,增彊閾值條件的描述能力,區分瞭枚舉型和數值型庫所,區分瞭普通遷移和彊賦值遷移,併給齣瞭擴展後的形式化定義及其和檢驗語言的語義映射.最後給齣在典型機載軟件上的應用,建立瞭軟件需求模型和部分映射代碼,對模型進行檢驗、反例路徑分析和需求完善.過程和結果錶明該方法可以有效的支持實際的關鍵安全軟件需求建模和驗證.
수구형식화건모화모형검험가이제고안전관건연건적가신성,단재모형묘술、조시화해석능력방면존재국한.대사용Petri망지지연건계통건모진행료확전,설정묵인치위령적권함수、이용"비"허선묘술재상태위가화변천실패정황하적촉발,증강역치조건적묘술능력,구분료매거형화수치형고소,구분료보통천이화강부치천이,병급출료확전후적형식화정의급기화검험어언적어의영사.최후급출재전형궤재연건상적응용,건립료연건수구모형화부분영사대마,대모형진행검험、반례로경분석화수구완선.과정화결과표명해방법가이유효적지지실제적관건안전연건수구건모화험증.
