Page 26 - 《软件学报》2025年第4期

1432 软件学报 2025 年第 36 卷第 4 期

但这并不代表其他的方法不能用.
其次, 在本文的研究中, 我们选择了时间自动机作为形式化模型, 从验证上来看, 我们的方法受限于时间自动
机的验证工具 UPPAAL 的验证能力. 从目前的验证上来看, 探索的状态空间在千万级别可以, 但是对于超过 10 亿
的状态空间, 就比较危险了. 对于我们的方法来说, 其解决方案在于需要将子验证系统的规模进行控制, 使得它的
验证空间不会过大, 这就对需求的分解有要求, 但如何分解出具有适当验证空间且有一定粒度的需求就成为一个
新的研究问题, 但这个不在本文的研究范围内.
关于依赖关系识别的完整性问题, 本文中关注了由于不同需求共享的数据和设备造成的数据依赖和控制依
赖. 至于是否还是有其他类型的依赖性, 我们目前并没有发现, 但不排除有的可能性. 在数据和控制依赖中, 我们充
分考虑了其可能的影响要素, 以保证依赖关系的完整识别. 其中数据依赖我们做了名唯一假设, 而控制依赖中我们
考虑的是需求的前置条件与需求对设备的控制, 这将充分识别需求由于设备的状态变迁带来的隐式关系. 我们认
为对于控制依赖的识别已经足够.
另外, 我们的方法并不局限于使用时间自动机. 在实际应用中, 可以根据需要选择不同的形式化模型. 关键在
于, 我们需要在第 3 步的验证系统模型中, 根据所选择的形式化模型的特性进行相应的替换和转换. 具体来说, 我

们需要能够对软件构件、设备构件和连接构件进行转换. 例如, 如果选择的是状态机模型, 那么就需要能够将软件
构件、设备构件和连接构件转换为相应的状态机. 如果选择的是过程代数模型, 那么就需要能够将这些构件转换
为相应的过程代数表达式. 这种灵活性使得我们的方法具有很好的可扩展性, 能够适应各种不同的应用场景, 具有
广泛的应用前景.
最后, 我们的方法构造的验证子系统是可执行的, 理论上来说它当然可以验证任何可以用 TCTL 描述的性质,
包括其他的安全性质. 但因本文的主题, 我们限制在了一些特定性质的表达上. 需要注意的是, 我们的验证子系统
是动态组装的, 它必须依赖于设备的 TA 模型. 在本文中, 假设验证的设备 TA 模型是提前构建好的. 这个假设是
可以成立的, 对于每个待验证系统, 其涉及的设备是确定的, 可以由领域专家与形式化专家提前构建在设备库中.
这并不妨碍本文方法的有效性.

6 结束语

本文提出了一种复杂嵌入式系统需求的一致性组合验证方法, 旨在有效约减验证系统的状态空间. 该方法的
核心在于充分挖掘需求间的依赖, 通过这些依赖实现对复杂嵌入式系统需求的有效分组, 从而有效构建验证子系
统, 并能够初步定位到不一致的需求. 在验证子系统的构建过程中, 我们制定了预期软件的 TA 模型, 并结合物理
设备模型进行动态构建, 它充分考虑了嵌入式系统需求的强物理设备性. 这种组合方法有效地减少了每个验证子
系统的验证状态空间, 提高验证效率, 并有助于定位不一致性. 我们进一步在航空领域的机载侦查系统中进行了实
证研究, 验证了该方法的实用性和有效性, 并通过 5 个案例评估, 证实了验证状态空间的显著减少. 这种组合验证
方法为复杂嵌入式系统需求的验证提供了一种实用的解决方案.
在未来工作中, 我们将考虑针对规模控制的需求分解, 使得分解对应的验证子系统的状态空间总是可以验证
的, 解除对验证工具的限制. 另外, 一方面考虑将本方法应用于更多实际的项目去, 检测其实际可用性. 另外一方
面, 拟针对更多的需求表示类型, 如 UML 顺序图等, 以及更多的性质进行验证, 对方法的应用面进行扩展, 使得方
法具有实用性.

References:
[1] Yang MF, Gu B, Duan ZH, Jin Z, Zhan NJ, Dong YW, Tian C, Li G, Dong XG, Li XF. Intelligent program synthesis framework and key
scientific problems for embedded software. Chinese Space Science and Technology, 2022, 42(4): 1–7 (in Chinese with English abstract).
[doi: 10.16708/j.cnki.1000-758X.2022.0046]
[2] Zowghi D, Gervasi V. On the interplay between consistency, completeness, and correctness in requirements evolution. Information and
Software Technology, 2003, 45(14): 993–1009. [doi: 10.1016/S0950-5849(03)00100-9]
[3] Chen XH, Zhong ZW, Jin Z, Zhang M, Li T, Chen X, Zhou TL. Automating consistency verification of safety requirements for railway