系统工程与电子技术
繫統工程與電子技術
계통공정여전자기술
SYSTEMS ENGINEERING AND ELECTRONICS
2012年
9期
1966-1972
,共7页
李震%刘斌%苗虹%殷永峰
李震%劉斌%苗虹%慇永峰
리진%류빈%묘홍%은영봉
软件工程%软件安全性%Petri网%形式化验证
軟件工程%軟件安全性%Petri網%形式化驗證
연건공정%연건안전성%Petri망%형식화험증
为了解决Petri网对复杂软件系统进行形式化验证时在安全性描述、自动化程度和验证效率方面存在的不足,提出一种软件安全Petri网.扩展了库所定义,提出了安全距离及其计算方法,以增强Petri网对软件安全性的描述能力.设计了自动划分子网结合库所安全定级的递归算法,仅对与被验证需求性质相关的划分子模型进行验证以提高验证效率,同时实现库所的安全定级.设计并实现了软件安全性需求自动化建模和验证工具原型,最后给出了在典型安全关键软件——机载除冰软件系统上的应用以说明方法和工具原型的有效性.
為瞭解決Petri網對複雜軟件繫統進行形式化驗證時在安全性描述、自動化程度和驗證效率方麵存在的不足,提齣一種軟件安全Petri網.擴展瞭庫所定義,提齣瞭安全距離及其計算方法,以增彊Petri網對軟件安全性的描述能力.設計瞭自動劃分子網結閤庫所安全定級的遞歸算法,僅對與被驗證需求性質相關的劃分子模型進行驗證以提高驗證效率,同時實現庫所的安全定級.設計併實現瞭軟件安全性需求自動化建模和驗證工具原型,最後給齣瞭在典型安全關鍵軟件——機載除冰軟件繫統上的應用以說明方法和工具原型的有效性.
위료해결Petri망대복잡연건계통진행형식화험증시재안전성묘술、자동화정도화험증효솔방면존재적불족,제출일충연건안전Petri망.확전료고소정의,제출료안전거리급기계산방법,이증강Petri망대연건안전성적묘술능력.설계료자동화분자망결합고소안전정급적체귀산법,부대여피험증수구성질상관적화분자모형진행험증이제고험증효솔,동시실현고소적안전정급.설계병실현료연건안전성수구자동화건모화험증공구원형,최후급출료재전형안전관건연건——궤재제빙연건계통상적응용이설명방법화공구원형적유효성.
