一种面向安全关键软件的AADL模型组合验证方法  

A Compositional Verification Method for AADL Models of Safety-Critical Software

作　　者：张博林 杨志斌[1,2] 周勇 马燕燕[1] 黄志球 薛垒[3] ZHANG Bo-Lin;YANG Zhi-Bin;ZHOU Yong;MA Yan-Yan;HUANG Zhi-Qiu;XUE Lei(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106;Key Laboratory of Software Development and Verification Technology Ministry of Industry and Information Technology for High Security Systems,Nanjing 210093;Shanghai Aerospace Electronic Technology Institute,Shanghai 201109)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]高安全系统软件开发与验证技术工信部重点实验室,南京211106 [3]上海航天电子技术研究所,上海201109

出　　处：《计算机学报》2020年第11期2134-2151,共18页Chinese Journal of Computers

基　　金：国家自然科学基金(61502231);国家重点研发计划(2016YFB1000802);GF基础科研重点项目(JCKY2016203B011);航空科学基金(201919052002);南京航空航天大学研究生创新基地(实验室)开放基金(KFJJ20181603)资助.

摘　　要：安全关键软件变得越来越复杂,这类软件的形式化验证是一个具有挑战性的问题.本文针对火箭发射控制子系统实例,提出一种组合验证方法,该方法采用组合验证与模型转换相结合的方法完成对该系统的验证与分析.首先,使用体系结构分析与设计语言AADL对火箭发射控制子系统进行层次化构造系统的体系结构模型,将系统各个层次的组件需求形式化为组件契约,然后通过组合验证确保系统体系结构的正确性;其次,提出了AADL2UPPAAL的模型转换方法,然后基于UPPAAL对该模型中组件的功能行为进行验证与分析,确保组件的功能行为的正确性;最后,实现了AADL模型验证原型工具,支持基于AGREE的体系结构模型的组合验证和支持基于UPPAAL的组件功能行为验证,通过对火箭发射控制子系统案例的验证和分析表明本文所提方法的有效性与局限性.The complexity of safety-critical software has been higher and higher with the development of requirement specification.Therefore,it is a serious challenge to verify whether these complex systems satisfy expected properties or not.According to the example of the rocket launch control subsystem,this paper proposes a combination of compositional verification and model checking to complete the verification and analysis of the system.First,Architecture Analysis and Design Language(AADL)is used to hierarchically construct the architecture model of the rocket launch control subsystem,and the component requirements of each level of the system are formalized by contract theory,and then the correctness of the system architecture is verified through compositional verification.Secondly,the functional behavior of the components in the model are verified based on UPPAAL to ensure the correctness of component behaviors;Finally,the AADL model verification prototype tool is implemented to support the compositional verification of AGREE-based architecture models and UPPAAL-based component functional behavior verification,the rocket launch control subsystem case is used to show the effectiveness and limitations of the proposed method are demonstrated.

关 键 词：安全关键软件 火箭发射控制子系统 组合验证 AADL UPPAAL 

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