(19)国家知识产权局 (12)发明 专利申请 (10)申请公布号 (43)申请公布日 (21)申请 号 202210421720.X (22)申请日 2022.04.21 (71)申请人 中国航空无线电 电子研究所 地址 200233 上海市徐汇区桂平路432号 (72)发明人 康介祥　王辉　崔杰　高忠杰　 尹伟　 (74)专利代理 机构 上海和跃知识产权代理事务 所(普通合伙) 31239 专利代理师 杨慧 (51)Int.Cl. G06F 8/10(2018.01) G06F 40/30(2020.01) G06F 16/22(2019.01) G06F 40/211(2020.01) G06F 40/253(2020.01) (54)发明名称 一种面向需求表格模型的形式化语义分析 与检查方法 (57)摘要 本发明公开了一种面向需求表格模型的形 式化语义分析与检查方法， 将 机载安全关键软件 的需求映射为基于命题逻辑与关系理论的数学 模型， 对其语义进行严格数学定义， 然后设计一 系列自动化算法来对需求的多层语义约束进行 验证。 权利要求书3页 说明书13页 附图4页 CN 114741052 A 2022.07.12 CN 114741052 A 1.一种面向需求表格模型的形式化语义分析与检查方法， 其特 征在于包 含以下步骤： 步骤一、 导入由条目需求转化而来的RTM模型； 其中一个RTM模型中包含以下集合： 数据 类型、 常量、 输入变量、 构型类、 内部变量、 输出变量、 表格函数， 表格函数分为三类， 分别 是 判断关系表、 激励关系表和构型转换表； 其中： 产生同类输出的一组判断型需求转化为一张判断关系表， 判断关系表的附属信 息中注 明需求共同影响的变量的变量名， 需求中产生的不同输出值各对应判断关系表中一行； 表 格的字段有： 所属构型、 判断条件、 输出值； 产生同类输出的一组激励型需求转化为一张激励关系表， 激励关系表的附属信 息中注 明需求共同影响的变量的变量名， 需求中产生的不同输出值各对应激励关系表中一行； 表 格的字段有： 所属构型、 激励、 输出值； 构型转换表对应模型中的每一个构型类， 它表示软件中各变量的取值发生了什么样的 变化时， 应该从哪个构型转换到哪个构型。 步骤二、 对RTM模型进行 各种分析。 2.根据权利要求1所述的一种面向需求表格模型的形式化语义分析与检查方法， 其特 征在于在进行输入层约束验证时， 包 含以下步骤： 2‑1)从RTM模型获得表格函数集 合， 遍历所有的表格函数； 2‑2)读取各判断关系表或激励关系表中的依赖构型类名称； 从RTM模型获得构型类集 合， 找到与依赖构型类名称匹配的构型类， 逐一加入第一构型集 合； 2‑3)遍历判断条件表或激励关系表的所有表格行， 读取各行表格行所属构型字段， 逐 一加入第二构型集 合； 2‑4)判断第一构型集合和第二构型集合是否相同， 如果不相同， 则说明有某些同类构 型未被判断关系表或激励关系表考虑到， 在出错信息中加入该表格违反输入层约束的提 示。 3.根据权利要求1所述的一种面向需求表格模型的形式化语义分析与检查方法， 其特 征在于在进行内部层的判断互斥约束验证时， 包 含如下步骤： 3‑1)从RTM模型获得表格函数集 合， 遍历所有的表格函数； 3‑2)若为判断关系表， 遍历所有表格行， 读取每行的所属构型， 将每个不同构型逐一加 入第三构型集 合； 3‑3)对第三构型集 合中的每 个构型， 进行 下述所有操作： 遍历判断关系表中所有判断条件字段中所属构型等于第 三构型集合中当前构型的行， 并解析判断条件， 整理以下数据结构： 被遍历各行的变量输出值、 判断条件， 判断关系表中 出现的每个不同的连续型变量， 以及每个连续型变量各对应一个出现在原子判断条件右侧 的取值集合， 判断关系表中出现的每个不同的离散型变量， 以及每个离散型变量各对应一 个其值域的所有取值 集合； 对于连续型变量对应的取值 集合， 将取值 集合中的值按从小到大排序； 对于每行判断条件， 将其中原子判断条件进行等 价替换， 将变量离 散化； 对所有变量的可能取值组合进行枚举， 组成析 取范式结构； 对析取范式进行扩充， 考虑每个合取式中未考虑到的变量， 对于每组变量可能取值， 和 原来的合取式组合 生成一个新 合取式， 用这些合取式替换掉原来的合取式；权　利　要　求　书 1/3 页 2 CN 114741052 A 2两两比较每一行判断条件化成的扩充式， 只要某两行存在相同的合取式， 说明当变量 取值为这样的取值组合时， 显然会同时满足这两行 的判断条件， 若这两行 的输出值还不相 同， 便是违反了判断互斥， 在出错信息中加入该表格 违反判断互斥的提 示。 4.根据权利要求3所述的一种面向需求表格模型的形式化语义分析与检查方法， 其特 征在于对原子判断条件进行等 价替换的方法如下： 对于包含离散型变量的原子判断条件， 将变量值域中每个取值从1开始编号， 用该编号 替换原子判断条件右侧的值； 对于包含连续型变量的原子判断条件， 用变量在各行判断条件中出现的取值集合中的 所有值将变量值域分段， 并将 每个区间从1开始编号， 然后用这些区间对应的取值范围替换 所有的原子判断条件。 5.根据权利要求1所述的一种面向需求表格模型的形式化语义分析与检查方法， 其特 征在于在进行内部层的判断完备性约束验证时， 包 含如下步骤： 4‑1)对某张判断关系表， 根据判断关系表的所有行的判断条件中出现的变量， 整理出 包含了所有变量所有可能取值组合的析 取范式； 4‑2)将所有行判断条件扩充后的析取范式进行析取， 将获得的析取范式与上一步的析 取范式相比较， 若不相等， 则说明判断关系表中存在未考虑到的取值组合， 当变量取值为这 种缺失的组合时， 判断关系表中没有任何一行判断条件被满足， 违反了判断完备性， 在出错 信息中加入该表格 违反判断完备性的提 示。 6.根据权利要求1所述的一种面向需求表格模型的形式化语义分析与检查方法， 其特 征在于在进行内部层的激励互斥约束验证时， 包 含如下步骤： 5‑1)遍历激励关系表， 获得激励关系表中的不同构型组成第一激励集 合； 5‑1)遍历所有激励关系表中构型结点值等于第 一激励集合中当前构型的行， 并解析激 励， 整理以下数据结构： 被遍历各行的变量输出值、 激励， 该行各AND激励的激励操作符、 守 卫操作符、 激励判断条件和守卫判断条件， 表格中出现的每个不同的连续型变量， 以及每个 连续型变量各对应一个出现在原子判断条件右侧的取值集合， 激励关系表中出现的每个不 同的离散型变量， 以及每 个离散型变量各对应一个其 值域的所有取值 集合； 5‑2)～C激励进行确定化处 理； 5‑3)对于连续型 各变量对应的取值 集合， 将取值 集合的值按从小到大排序； 5‑4)对于各 行各AND激励的激励判断条件和守卫判断条件替换为 一个析取范式； 5‑5)将激励等 价为前一时刻满足的判断条件P和后一时刻满足的判断条件P ’； 5‑6)将每行处理完的每个AND激励， 把P和P ’全部合取， 得到能够满足该行激励的两个 判断条件， 当某个瞬间变量取值组合满足判断条件1， 下个瞬间变量取值组合满足判断条件 2时， 则视为该 行激励发生； 5‑7)两两比较每一行激励化成的两个析取范式， 若两个式子都分别存在相同的合取 式， 说明当某瞬间变量取值为第一个式子同时存在的取值组合， 下一瞬间变量取值为第二 个式子同时存在的取值组合时， 显然会同时满足这两行 的激励， 若这两行 的输出值还不相 同， 便是违反了内部层的激励互斥约束， 在出错信息中加入该表格违反内部层的激励互斥 约束的提 示。 7.根据权利要求6所述的一种面向需求表格模型的形式化语义分析与检查方法， 其特权　利　要　求　书 2/3 页 3 CN 114741052 A 3