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

摘要 嵌入式软件在安全关键领域的广泛运用使得保障软件安全性成为工业界和学术界关注的重要课题.抽象解释作为一种形式化方法为程序变量的数值分析提供了一种通用框架，八边形抽象域是抽象解释的一种关系型数值抽象域，可以表示两个变量间的数值关系.基于八边形抽象域设计了一个对程序变量进行数值分析的原型工具，并利用此工具对襟缝翼控制系统的安全性展开研究，包括：利用抽象解释框架对襟縫翼系统的中断驱动进行建模；通过迭代计算程序中各个节点的数值不变式，检测程序中与数值相关的错误；根据分析结果对产生错误的代码进行定位.本文将抽象解释理论应用到航空控制软件的安全分析中，并提供了一种对程序中数值变量进行自动化分析的途径