Modeling and verification of software safety requirement based on ontology
-
摘要: 由软件引起的灾难性事故原因往往源于安全性需求,目前主观的人工评审方法并不能满足软件安全性需求严格的验证要求.因此,讨论了软件安全性需求的定义,遴选了国内外公认的相关标准和手册作为需求验证的知识基础,根据"七步法"建立了本体模型,利用本体模型中的概念和关联来形式化地描述规则以支持验证;同时基于以上研究内容设计和实现了软件安全性需求形式化建模和验证的工具原型,并对使用工具实施验证和使用人工评审实施验证进行了对比分析实验.实验结果表明形式化工具原型在验证时间和验证次数上都大大优于人工验证方法,同时工具原型具有良好的易用性.Abstract: The catastrophic accidents are usually caused by and related to safety requirement and the manual review cannot meet the strict verification requirement of software safetyd.Consequently, the definition of software safety was discussed, the recognized and related standards with guidebooks were strictly selected as the knowledge bases of requirement verification, the ontology models were built by "seven step method", the rules were formally described by the concepts and relations in ontology models to support verification, the tool prototype of formal modeling and verification of software safety requirement was designed and realized, and the tool prototype was used to the comparative experiment between manual verification and automatic verification. The result of the experiment shows that using tool prototype is far better than manual verification in time consumed, verification times and the prototype has a good usability as well.
-
Key words:
- software safety /
- ontology /
- formal verification
-
[1] Gerard L L.An analysis of the ariane 5 flight 501 failure-a system engineering perspective [C]//Proceedings of the 1997 Workshop on Engineering of Computer-Based Systems.NY:IEEE Press,1997:339-346 [2] 王继军.胶济客运专线信息安全传输系统方案改进[J].铁路通信信号,2009,45(6):54-55 Wang Jijun.The improvement of system information safety transition of qingdao-jinan line[J].Railway Signaling & Comunication,2009,45(6):54-55(in Chinese) [3] 马李灵珊,刘琳.死亡动车[J].南方人物周刊,2011(26):30-34 Mali Linshan,Liu Lin.Fatal EMU[J].Southern People Weekly,2011(26):30-34(in Chinese) [4] Leveson N G.Software safety:why,what,and how [J].ACM Computing Surveys,1986,18(2):125-163 [5] Gregory Zoughbi.A UML profile for developing airworthiness-complaint (RTCA DO-178B) safety-critical software[M].Ottawa,Canada:Carleton University,2006 [6] Std 610.12-1990 IEEE standard glossary of software engineering terminology[S] [7] GJB-438B 2009 军用软件开发文档[S] GJB-438B 2009 Military software development documents[S](in Chinese) [8] 邓志鸿,唐世渭,张铭,等.Ontoglogy研究综述[J].北京大学学报:自然科学版,2002,38(5):730-738 Deng Zhihong,Tang Shiwei,Zhang Ming,et al.Overview of ontology[J].Acta Scicentiarum Naturalum Universitis Pekinesis:Natural Science Edition,2002,38(5):730-738(in Chinese) [9] 钟秀琴,符红光, 佘莉,等.基于本体的几何学知识获取及知识表示[J].计算机学报,2010,33(1):167-174 Zhong Xiuqing,Fu Hongguang,She Li,et al.Geometry knowledge acquisition and representation on Ontology[J].Chinese Journal of Computers,2010,33(1):167-174(in Chinese) [10] 李景,苏晓鹭,钱平. 构建领域本体的方法[J]. 计算机与农业,2003(7):7-10 Li Jing,Su Xiaolu,Qian Ping.The methodology of developing domain ontology[J].Computer and Agriculture,2003(7):7-10(in Chinese) [11] ptc/07-08-04 A UML profile for MARTE,beta 1[S] [12] ptc/04-09-01 UML profile for modeling quality of service and fault tolerance characteristics and mechanisms[S] [13] formal/05-01-02 UML profile for schedulability,performance,and time specification[S] [14] Wolforth I,Walker M,Papadopoulos Y.A Language for failure patterns and application in safety analysis [C]//Dependability of Computer Systems.NY:IEEE Computer Society,2008:47-54
点击查看大图
计量
- 文章访问数: 1813
- HTML全文浏览量: 65
- PDF下载量: 851
- 被引次数: 0