摘要
如何对软件需求展开有效验证是当前国内民机系统安全攸关软件研发过程中的重要挑战.本文对基于变量关系模型VRM(Variable Relation Model)的机载软件需求形式化建模与验证过程中出现的状态空间爆炸问题,提出了一个面向VRM需求模型的状态空间等价语义划分准则和形式化组合验证方法框架,包括:基于VRM模型的结构和语义,构建变量依赖图VDG(Variable Relation Graph);设计了多个独立性划分算法将模型划分为若干独立的子模型;同时考虑所需验证的属性公式中的变量依赖关系,提出了一种属性驱动的独立性划分方法,并证明了划分前后模型状态空间的语义等价性;最后建立了从VRM模型转换到SMV模型的流程,并给出了一个机载软件系统需求建模与验证的实例研究.
How to effectively verify software requirements is an important challenge in the process of developing safety-critical software of domestic civil aircraft systems..Aiming at the state explosion problem during the formal requirement modeling and verification of airborne software based on Variable Relation Model(VRM),this paper proposes the state space equivalence semantic partition criterion and the framework of the formal compositional verification method for the VRM requirement model.Firstly,based on the structure and semantics of the VRM,the Variable Relation Graph(VDG)is constructed,then we design the independence partition algorithm to divide the model into several independent sub-models.Considering the dependencies of variables in the properties to be verified,we design the property based independence partition method,and prove the semantic equivalence of the model state space before and after partitioning.In addition,a framework of converting from VRM model to SMV model is established.Finally,an example of the requirement modeling and verification of an airborne software system is given.
作者
戴嘉磊
胡军
董亚炯
董泽华
王立松
DAI Jialei;HU Jun;DONG Yajiong;DONG Zehua;WANG Lisong(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Collaborative Innovation Center of Novel Software Technology and Industry,Nanjing 210007,China)
出处
《小型微型计算机系统》
北大核心
2026年第1期193-200,共8页
Journal of Chinese Computer Systems
基金
国家自然科学基金重点项目(U224120044)资助。
关键词
软件需求验证
安全攸关软件
模型检测
状态空间爆炸
模型划分
software requirements verification
safety-critical software
model checking
state explosion
model partitioning
