一种面向航电系统的基于需求的形式化建模与验证方法

摘要

本发明公开了一种面向航电系统的基于需求的形式化建模与验证方法，该方法运用需求状态机语言RSML^‑e建立系统的形式化需求模型，给出形式化模型转换规则，将RSML^‑e模型转换为模型检测器的输入模型，验证系统的安全性质，提升了系统的安全性和可靠性，同时也节省了时间和成本。

主权项

一种面向航电系统的基于需求的形式化建模与验证方法，其特征在于，包括以下步骤：(1)采用形式化需求状态机语言RSML^‑e对航空电子系统进行形式化需求规约，创建航空电子系统的形式化模型，并在建模过程中发现系统描述中的错误；(2)选择支持自动化验证的模型检测器，并给出形式化模型的转换规则，将步骤(1)构建的形式化模型根据转换规则转换为选择的模型检测器的输入模型；(3)将步骤(2)得到的模型检测器的输入模型和用户提出的航天电子系统的属性规约输入模型检测器，判断构建的形式化模型是否满足用户提出的属性规约，从而验证形式化模型的安全性质，并将验证结果反馈给用户。