一种面向SCR需求模型的形式化验证方法研究  

Formal Verification Method for SCR Requirement Model

作　　者：张漾 胡军[1,2] 王立松 康介祥[3] 王辉 高忠杰[3] ZHANG Yang;HU Jun;WANG Li-song;KANG Jie-xiang;WANG Hui;GAO Zhong-jie(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Collaborative Innovation Center of Novel Software Technology and Industrialization,Nanjing 210007,China;China National Aeronautic Radio Electronics Research Institute,Shanghai 200233,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]软件新技术与产业化协同创新中心,南京210007 [3]中国航空无线电电子研究所,上海200233

出　　处：《小型微型计算机系统》2022年第1期193-202,共10页Journal of Chinese Computer Systems

基　　金：国家“九七三”重点基础研究发展计划项目(2014CB744900)资助。

摘　　要：在需求层级进行建模分析与验证是复杂安全关键软件开发过程中的核心关注点.本论文工作面向航空领域中典型安全关键软件的需求层级,提出了一种基于形式化模型检验技术的需求模型验证方法.首先分析了形式化需求模型(SCR)的建模工具(T-VEC)中所定义的递归结构形式的模型语法与语义,提出了一种对模型变量关系进行平展化的方法,将SCR表格关系模型转换为自动机状态迁移图,然后设计了从SCR模型到模型检验工具(nuXmv)的模型自动转换框架,并对模型转换规则给出了严格的定义证明;最后通过一个航空软件系统的需求实例展示了方法的有效性.Modeling analysis and verification at the requirement level are the core concerns in the development of complex safety-critical software.Based on formal model verification technology, this thesis puts forward a requirement model verification method about typical safety-critical software for aviation.Firstly, this essay analyzes the model recursive syntax and semantics, which are defined by modeling tool(T-VEC)in the formalized requirement model(SCR).Secondly, it proposes a method to flatten the relationship between the model variables, and makes regulations to transform the SCR tabular relationship model into an automaton state migration diagram.Then this article design an automatic model conversion framework from the SCR model to a model verification tool(nuXmv),and give strict reasons to prove definition of the model conversion rules are correct.Finally, an example of the requirements of an aviation software system is passed to show the effectiveness of the method.

关 键 词：安全关键系统 nuXmv模型 模型映射 安全性验证 

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