计算机技术与发展2017，Vol.27Issue(6)：7-10,4.DOI:10.3969/j.issn.1673-629X.2017.06.002
基于需求的形式化建模与验证方法研究
Investigation on Formal Modeling and Verification MethodBased on Specification
摘要
Abstract
In the process of software development,the mistakes introduced in requirements phase have a more significant effect of the security and reliability than the phase of designing.In order to be able to detect the errors in the early phase of the software development and reduce development costs,and to describe the software system precisely and concisely,a formal modeling and verification framework has been proposed with the technology of automatic verification,in which the RSML-e model has been used and then the formal transformation rules have been given.Based on these rules,the proposed model can be transformed into the input model of the NuSMV,which is performed in model checking of the system.The specific instances of avionics system have been employed to implement modeling test experiments for verification.The experimental results show that the security and reliability of the established avionics system have been verified to be effective.关键词
形式化方法/RSML-e/模型检测/NuSMVKey words
formal method/RSML-e/model checking/NuSMV分类
信息技术与安全科学引用本文复制引用
李勇,曹子宁..基于需求的形式化建模与验证方法研究[J].计算机技术与发展,2017,27(6):7-10,4.基金项目
国家"973"重点基础研究发展计划项目(2014CB744900) （2014CB744900）
航空科学基金(20150652008) （20150652008）
