由软件引起的灾难性事故原因往往源于安全性需求，目前主观的人工评审方法并不能满足软件安全性需求严格的验证要求．因此，讨论了软件安全性需求的定义，遴选了国内外公认的相关标准和手册作为需求验证的知识基础，根据“七步法”建立了本体模型，利用本体模型中的概念和关联来形式化地描述规则以支持验证；同时基于以上研究内容设计和实现了软件安全性需求形式化建模和验证的工具原型，并对使用工具实施验证和使用人工评审实施验证进行了对比分析实验．实验结果表明形式化工具原型在验证时间和验证次数上都大大优于人工验证方法，同时工具原型具有良好的易用性．%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 con- sumed, verification times and the prototype has a good usability as well.
展开▼
