复杂嵌入式系统需求一致性的组合验证方法  

Compositional Verification for Requirements Consistency of Complex Embedded Systems

作　　者：杨晓[1] 王小齐 陈小红[1] 金芝[2,3] YANG Xiao;WANG Xiao-Qi;CHEN Xiao-Hong;JIN Zhi(Shanghai Key Laboratory of Trustworthy Computing(East China Normal University),Shanghai 200062,China;Key Lab of High Confidence Software Technologies(Peking University),Ministry of Education,Beijing 100871,China;School of Computer Science,Peking University,Beijing 100871,China)

机构地区：[1]上海市高可信计算重点实验室(华东师范大学),上海200062 [2]高可信软件技术教育部重点实验室(北京大学),北京100871 [3]北京大学计算机学院,北京100871

出　　处：《软件学报》2025年第4期1413-1434,共22页Journal of Software

摘　　要：形式化方法在需求一致性验证领域已经取得了显著的成就.然而,随着嵌入式系统需求复杂度的不断提升,需求一致性验证面临着状态空间过大的挑战.为了有效约减验证的状态空间,同时考虑到嵌入式系统需求所涉及的设备强依赖性,提出一种复杂嵌入式系统需求一致性的组合验证方法.它基于需求分解,识别需求间的依赖关系,通过这些依赖关系组装验证子系统,从而实现对复杂嵌入式系统需求的组合验证,并能初步定位到不一致的需求.具体而言,采用问题框架方法对需求进行建模和分解,并预设领域设备知识库对设备的物理特性进行建模.在验证子系统的组装过程中,生成预期软件的行为模型,并结合物理设备的模型进行动态组装.最后,采用航空领域机载侦查系统进行了实例研究,验证了方法的可行性和有效性,并通过5个案例评估证实了验证状态空间的显著减小.此方法为复杂嵌入式系统需求的验证提供了一种切实可行的解决方案.Formal methods have made significant strides in the field of requirements consistency verification.However,as the complexity of embedded system requirements continues to increase,verifying requirements consistency faces the challenge of dealing with an excessively large state space.To effectively reduce the verification state space,while also considering the strong dependency among devices in embedded system requirements,this study proposes a compositional verification method for ensuring the consistency of requirements in complex embedded systems.This method is based on requirement decomposition and identification of dependencies among requirements.By leveraging these dependencies,it assembles verification subsystems,enabling the compositional verification of complex embedded system requirements and facilitating the initial identification of inconsistencies.Specifically,the problem frames approach is employed for requirement modeling and decomposition,while a domain-specific device knowledge base is utilized for modeling the physical characteristics of devices.During the assembly of verification subsystems,models of expected software behavior are generated and dynamically integrated with physical device models.Finally,the feasibility and effectiveness of this method are validated through a case study of an airborne reconnaissance control system,demonstrating a significant reduction in the verification state space through five case evaluations.This method thus provides a practical solution for verifying the requirements of complex embedded systems.

关 键 词：复杂嵌入式系统 需求一致性 组合验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]