基于八边形抽象域的襟缝翼控制系统安全性分析  

Safety Analysis for Slats and Flaps Control Unit Based on Octagon Abstract Domain

作　　者：陆陈[1] 黄志球[1] 阚双龙[1] 曹德建 黄传林 

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016

出　　处：《小型微型计算机系统》2016年第5期902-907,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61100034;61170043)资助;中国博士后科学基金项目(20110491411)资助;江苏省研究生培养创新工程项目(KYLX_0315)资助;江苏省普通高校研究生科研创新计划项目资助;中央高校基本科研业务费专项资金项目(CXZZ11_0218)资助

摘　　要：嵌入式软件在安全关键领域的广泛运用使得保障软件安全性成为工业界和学术界关注的重要课题.抽象解释作为一种形式化方法为程序变量的数值分析提供了一种通用框架,八边形抽象域是抽象解释的一种关系型数值抽象域,可以表示两个变量间的数值关系.基于八边形抽象域设计了一个对程序变量进行数值分析的原型工具,并利用此工具对襟缝翼控制系统的安全性展开研究,包括:利用抽象解释框架对襟縫翼系统的中断驱动进行建模;通过迭代计算程序中各个节点的数值不变式,检测程序中与数值相关的错误;根据分析结果对产生错误的代码进行定位.本文将抽象解释理论应用到航空控制软件的安全分析中,并提供了一种对程序中数值变量进行自动化分析的途径.With the widespread use of embedded software in safety critical system, software safety assurance becomes an important issue from both academia and industry. Abstract interpretation as a formal method provides a general framework for the numerical analysis of program variables. The octagon abstract domain is a relational numerical abstract domain for static analysis that is able to represent and manipulate two invariants. This paper develops a prototype tool for numerical analysis based on the octagon abstract domain, and formally analysis an interrupt-driven Slats and Flaps Control Unit software programmed in C using the prototype,including：modeling the Slats and Flaps Control Unit software based on the abstract interpretation framework,discovering numerical errors by iterative calculation of numerical invariants of each node in the program, error positioning according to the results of the analysis. This paper applies the abstract interpretation theory to the practice of safety analysis for aircraft controller software and provides a way to automatically analysis numerical variables of programs.

关 键 词：抽象解释 八边形抽象域 数值分析 航空控制软件 

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