软件开发过程中需求阶段的错误比设计或实现阶段所引入的错误对系统的安全性与可靠性有更大的影响.为了能够在早期发现错误,降低开发成本,精确、简明地验证和规范软件系统和性质,在模型的形式化开发方法和模型检测的自动验证技术的研究基础上,提出了一种基于需求的形式化建模与验证的框架.运用基于四变量模型的需求状态机语言RSML-e建立了形式化模型,并给出了形式化的转换规则,将RSML-e模型转换为模型检测器NuSMV的输入模型,并进行了检测,建立起了一套整体的形式化开发框架,并以航空电子系统特定实例进行了建模与验证.验证结果表明,已建航电系统模型的安全性和可靠性是有效的.%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.
展开▼
