许婧祺，董龙明，郝丽波

（1.湖南机电职业技术学院，长沙410073；2.总装备部驻南京地区军事代表室，南京210000）

军用指挥控制软件可信性分析与验证技术*

许婧祺1，董龙明2，郝丽波1

（1.湖南机电职业技术学院，长沙410073；2.总装备部驻南京地区军事代表室，南京210000）

随着武器装备信息化程度越来越高，军用指挥控制软件的可信性直接关系到装备整体效能的发挥。在对传统软件质量保证技术研究的基础上，结合军用指挥控制软件的特点，提出了基于形式化方法的软件分析与验证技术。分别从安全性质形式化规约技术、基于模型检验的指挥软件验证技术和基于静态分析的控制软件分析技术三方面保证军用指挥控制软件的可信性，最后，提出了适用于指挥控制软件全生命周期开发的形式化分析与验证集成环境。

军用指挥控制软件，分析与验证技术，模型检验，静态分析

0　引言

随着新军事变革的深入，武器装备的信息化、智能化程度越来越高，软件在整个武器系统中扮演的角色越来越重要，例如：数值计算、信息处理、智能决策、行为控制等，无不存在着软件的身影。在高技术战争过程中，软件起着无可替代的作用，大至战役规划、战场决策，小到诸元标定、指令下达、武器装备单元控制等。在体系作战中，软件产品负责信息收集、加工、处理、储存、分发等任务，将各个独立的武器装备互联互通成一个有机的整体。软件的复杂性也将会进一步增加，对软件功能和安全性的要求也会越来越高，其正确性和可信性直接关系到武器系统的有效性，甚至直接关系到战争的胜负。一方面，我们感受着软件带来的好处，同样的武器硬件平台，由于软件的改进，武器系统反应时间、打击的精度和杀伤力大幅提高；另外一方面，随着武器系统功能越来越复杂，软件规模越来越大，软件质量难以得到保证。武器系统中某个软件模块的缺陷或错误可能导致整个武器系统的失效，甚至导致重大经济损失和人员的伤亡。例如：1996年，欧洲空间局的阿丽亚娜火箭发射37 s后爆炸导致6亿美元的损失是由于在一个64位浮点整数转换为16位有符号整数时产生溢出。美国国家标准技术研究所发布报告，2002年美国由于软件缺陷而引起的损失额高达592亿美元，占美国国内生产总值的0.6%。因此，总装备部为了提高军用软件质量，制定了国军标GJB 4072A-2006《军用软件质量监督要求》［1］，规定了军用软件研制整个过程的质量监督的依据、目的、原则和要求，明确软件质量监督全过程管理的规范，但是没有说明在软件研制各个过程中可以使用的软件质量保证技术。软件安全性（Safety）［2］是指在规定的条件下、规定的时间内，软件运行不引起任务失败、人员伤亡、造成重大政治影响或者经济损失等系统事故的能力。本文针对陆军指挥控制软件的机理及安全性要求，在分析传统软件质量保证技术不足的基础上，提出软件可信性保证形式化分析与验证技术。

1　传统软件质量保证技术

1.1军用软件成熟度模型

软件能力成熟度模型（Capability Maturity Model for Software，CMM）［3-4］是对软件组织在定义、实现、度量、控制和改善其软件过程的进程中各个发展阶段的描述，本质是通过履行一系列的关键过程域中关键实践来达到软件过程的目的。CMM可以分为5个等级：

（1）初始级。它的软件过程管理处于无序的、混乱的状态，软件项目的成功完全依赖于个人能力和团队的合作，软件的进度、质量、预算均不可测。

（2）可重复级。它的主要特征是已经建立了管理软件项目的方针和实施这些方针的规程。软件组织要对正在实施的和已经实施的软件项目进行经验总结，从而抽象出软件过程实施当中有效的、具体的、适用的方法，并将其文档化，形成规程，为以后的项目预算、评估和软件过程实施提供依据。通过执行已文档化的规程，对当前项目形成有效的控制，产生稳定的软件过程能力。

（3）已定义级。它的主要特征是标准化。已定义级与可重复级相比，更强调软件开发各有关组织的相互协调和作为一个统一的整体参与软件的开发。在这一等级上，组织开发和维护软件的过程已经文档化，软件工程过程和软件管理过程被综合为一个有机的整体，称为标准软件过程。通过剪裁标准化软件过程和适当地修改，产生文档化的项目的软件过程。这样每一个项目软件过程都是从标准软件过程发展而来，它们是稳定的、可重复的，成本、进度及软件质量处于一定的受控状态。

（4）已管理级。它的特征是定量化。组织对软件产品和过程设置定量的质量目标，并限定这些目标的变化范围。整个等级的软件过程有妥善的定义和一致的度量尺度，组织的软件过程能力可以预测，对于新领域的软件过程控制，软件成熟度模型CMM描述项目开发工作也可以评测其风险。

（5）优化级。它的特征是对软件过程的不断改进，从而使软件过程能力不断提高，软件缺陷得到预防。通过对以往的软件过程分析，鉴别各种技术革新，并选择最优的进行推广。

1.2软件测试技术

软件测试是软件开发过程中十分重要的步骤，是保证软件功能正确的重要过程。根据软件开发周期阶段进行划分，软件测试一般可以划分为单元测试、集成测试、系统测试、验收测试和回归测试。根据测试用例（也称为测试数据）的选择或产生方法不同，动态测试又可以分为基于规范的测试（又称为黑盒测试或功能测试）、基于程序的测试（又称为白盒测试或结构测试）以及规范与程序的联合测试。基于规范的测试指根据软件规范或软件输入输出关系产生测试用例，并判断测试结果的正确性（也称为进行测试失效辨识）；基于程序的测试则需要根据程序的内部结构特征和与执行路径相关的数据特征产生测试用例。除了基本的功能性测试外，还要考虑对软件的许多非功能性需求进行测试，包括性能测试、兼容性测试、用户界面测试、多语言测试、安全性测试、可靠性测试、安装测试等等。

2　基于形式化方法的指挥控制软件分析与验证技术

软件成熟度模型是通过第三方从软件工程领域规范软件开发人员的行为和流程；软件测试技术是设计测试案例验证软件产品满足用户需求、实现合同中的功能，是一种标准化流程标准，从软件开发流程规范软件开发人员的行为，从规章制度上杜绝软件开发过程中可能的出错。软件测试技术自动化程度比较高，有许多成熟的自动化方法和工具，是当前工业界常采用的方法，但是受限于测试案例的设计和覆盖率，不能完全保证该软件没有缺陷和错误软件。形式化分析与验证方法能够完全证明软件在任何条件下没有错误，但是对软件质量保证人员要求比较高，需要比较深的数学和逻辑功底，能够建立软件各种规范化模型和逻辑推理能力，是当前学术界研究比较多的方法。

2.1安全性质形式化规约技术

对软件进行形式化验证的主要目的就是验证软件是否满足某些目标性质。这些目标性质分为安全性（Safety）和活性（Liveness）两大类，安全性是指软件在运行过程中不发生非预期的行为，如运行时不发生崩溃等；活性是指预期的行为在软件的运行过程中总会发生，如程序的终止性等。

在指挥控制软件的实际开发与应用中，用户往往在软件的功能和行为级描述所需的安全性质。为了能够分析和验证软件是否满足这些性质，首先需要研究如何将用户的顶层需求模型转换和映射为等价的、源代码级可体现的性质。例如，“软件运行时不会崩溃”这一安全性质映射到源代码级实际上包括无算术溢出、无除零错、无数组越界、无空指针引用等性质。将安全性质映射到软件源代码层面以后，还需要研究如何采用精确、严格的方式对其进行形式化规约，为形式化分析和验证过程提供目标。

军用指挥控制软件涉及到两类安全性质，一类是模型级时序性质，一类是源代码级的运行时错误。时序性质主要指指挥软件中用户对某些操作的序列有所规定。时序性质对于刻画指挥软件中的常见反应式性质，比如“p操作发生后q操作一定将会发生”。时序性质适合于描述关于并发的一些性质，比如没有死锁。源代码级的运行时错误指武器控制程序在运行过程中可能发生的错误，武器控制软件中的运行时错误一般包括：算术溢出、数组访问越界、无效算术操作（除零错、对负数开平方根等）、访问未初始化变量、空指针引用等。

军用指挥控制软件安全性质形式化规约方法有3种：第1种是基于可达性（Reachability）的性质规约描述方法；第2种是基于自动机的性质规约描述方法；第3种是基于时序逻辑的性质规约描述方法。这3种性质规约方法具有不同的特点，适合不同的应用。基于可达性的性质规约描述方法最为简单，它描述的是软件源代码中某个程序点（比如某个判断用户指定性质出错的位置）在软件的运行过程中可达或不可达，但其描述能力较弱不适合描述复杂的时序性质。基于自动机的规约描述方法的描述能力是足够强的，它可以描述软件的时序和并发性质，而且表示直观、处理方便，因此，得到了广泛的应用，如有穷自动机、下推自动机等。基于时序逻辑的规约描述方法的描述能力也较强，表示形式也比较简洁直观，但一般情况下描述能力弱于基于自动机的规约描述方法，如LTL［5］、CTL［6］等。

2.2基于模型检验的指挥软件形式化验证技术

下一代指挥系统逐渐向网络中心化系统发展，是一个复杂人机系统，常见的系统建模理论和方法包括：Petri网［7］、影响图［8］、Lanchester方程［9］、多智能体系统［10］以及复杂网络［11］，对指挥作战中各要素进行建模，生成各种模型，例如：指挥关系模型、作战活动模型、作战规则模型、系统接口模型、系统通信模型等，分析指挥软件系统中关键性软件系统的实时性、可靠性、可用性、安全性等可信属性，从作战视图、系统视图、技术视图等多个层次，发现和提取有待验证的与实时性和可用性相关的可信性质。

对指挥软件进行建模常常涉及到的软件模型包括：各类UML模型和自动机、Petri网、进程代数等形式化模型。模型检验技术包括：面向各类形式模型的检验技术、面向各类UML模型的检验技术、面向多视图建模方法的行为一致性检验技术、基于前后置谓词的程序正确性证明技术。

2.3基于静态分析的控制软件源代码形式化分析技术

静态分析是指在不运行软件前提下进行的分析，对象一般是针对程序源代码，也可以是目标代码。基于源代码的分析一般是基于某个开源编译器，利用分析前端得到抽象语法树，在控制流图、或数据流上进行各种类型的分析和检查。基于格（lattice）和不动点（fixpoint）理论的数据流分析是目前广泛采用的技术：首先对控制流图中每个结点建立一个数据流等式，并根据分析目标构造一个具有有限高度的格L，然后不断重复计算每个节点的输出，直到达到格的一个不动点。

图1　符号执行框架

基于符号执行技术的程序源代码分析框架［12］如图1所示。首先，利用开源编译器前端将待分析的软件成品功能模块源程序解析成各种计算机可存储和理解的中间形式，如：抽象语法树、符号表、函数调用图、控制流图等形式。其中，控制流图（CFG）是用有向图表示一个程序过程控制结构的抽象数据结构，图中的节点表示一个程序基本块，边表示代码中的跳转。符号调度器是基于每种特定程序符号值的操作语义在控制流图边指向上依次模拟调度执行每条语句，在遇到分支节点时，使用约束求解器判定哪条分支可行，并得到一组可执行路径的关于程序变量的解。当所有控制流图上所有节点和边遍历结束时，就能得到覆盖所有可执行路径的一组关于程序变量的数据。

在符号执行框架中，有两种技术影响符号执行框架的效率：

1）符号调度器。通常基于有向图搜索策略的不同可以分为：深度遍历和宽度遍历。当前，符号调度器比较有名的研究性成果有EXE、JPF-SE、KLEE等等。

2）约束求解器。是获取满足一组约束的解，典型代表性工具有SAT/SMT求解器。随着约束求解技术飞速发展，已经能够解决实际领域中许多问题，例如：符号执行工具KLEE调用STP约束求解器求解所有路径的约束条件真值；Z3已成功应用于微软项目Spec#/Boogie中。

使用静态分析检测方法对控制类软件程序进行检测，可以分析内存安全性相关的错误，例如：内存泄漏、空指针解引用、悬挂指针解引用、多次释放，研究各类Lanchester方程设计约束求解器，得到一组能覆盖各类解算程序所有执行路径的用例，用于软件测试过程，能够覆盖所有测试路径。

2.4指挥控制软件形式化分析与验证集成环境

以上述研究技术为基础，设计并实现相应的分析与验证集成环境，用在指挥控制软件设计与开发过程中，能够有效对指挥控制软件关键模块进行形式化分析与验证，并具有较高的自动化程度。指挥控制软件形式化与验证集成环境框架如图2所示，主要包括安全性质形式化规约技术、基于模型检验的形式化验证技术、基于静态分析的源代码形式化分析技术。底层关键支撑技术包括性质规约、自动模型抽象与验证、C程序语义抽象内存模型、基于抽象模型的静态检测技术等。

图2　指挥控制软件形式化分析与验证集成环境框架

本项目拟设计的验证支撑环境包括两部分：①基于模型检验的验证工具，如图3所示；②基于内存抽象模型的程序静态分析工具，如图4所示。

图3基于模型检验的验证框架

图3给出了本项目拟设计的基于模型检验的程序验证框架。从功能上，该框架主要包括如下2个模块：模型抽象算法和模型检验模块。

1）模型抽象算法：基于给定的谓词集合，采用谓词抽象，从各指挥类软件设计过程生成的各类模型中抽取有穷状态抽象模型（如：布尔程序）；

2）模型检验模块：对抽取出的模型使用模型检验算法进行状态搜索，如果性质成立，则验证过程结束，软件源代码满足给定的性质；否则，对模型检验算法产生的反例进行可行性检查和处理。

图4　基于内存抽象模型的静态程序分析框架

图4给出了本项目拟设计的基于内存抽象模型的静态程序分析框架［13］。从功能上，该框架包括如下4个模块：

1）内存抽象模型：针对堆操作程序关于指针操作具有局部特性，以与指针指向结点距离值为分界点精确描述和保守抽象指针的别名关系，保证分析不产生漏报，同时达到一定的可扩展性。

2）内存泄露检测Memcheck：内存泄漏是软件可信性研究的重要内容，同时是指针操作程序易发生、难以检测的错误。平凡的指针域操作、各种数据结构交织在一起更增加了检测它的难度。以内存抽象模型为程序状态，根据程序的操作语义对程序状态进行迁移，找到各个程序点关于程序状态的不动点，对控制软件程序进行自动检测内存泄漏错误。

3）非法指针解引用检测Pointercheck：非法指针解引用是软件可信性研究的另一重要内容，它可能会导致信息泄漏、重要数据被篡改或系统崩溃。程序运行过程中表现形式又可以具体分为3种类型：空指针解引用、悬挂指针解引用、多次释放。这3种类型的错误既有统一的一面，又有区别的一面：相同的是指针的值是无效的（即：所指向的内存结点已经被释放），因此，这3种类型错误检测能够统一于同一个抽象模型；不同的是这3种类型发生的形式不同，这就需要针对不同语句设计违背合法指针解引用规则进行分类检测。以内存抽象模型为程序迁移状态，以3种非法指针解引用发生的条件为检测依据，对控制软件程序进行非法指针解引用的算法。

4）数值性质检测Numcheck：装备控制软件涉及到大量的基于Lanchester方程诸元解算程序，运算过程中这些数据在计算机中由浮点数表示的，浮点数具有非均匀分布特征，并且浮点操作会引入浮点误差。尽管单个浮点操作所带来的舍入误差通常都很小，但如果舍入误差在长序列的浮点计算中不断累加时，也可能产生严重后果，甚至导致灾难性后果。数值性质检测将研究如下安全性相关问题：①分析浮点程序是否会出现上溢、除零错、无效运算等运行时错误；②分析浮点程序中舍入误差的传播情况，并分析程序中舍入误差的源头及累计上界。

3　结束语

随着武器装备信息化程度的提高，军用软件的规模逐渐增大，复杂度也逐渐增加，在软件开发各个阶段使用软件质量保证技术可以增强软件的可信性，提高武器系统的稳定性和可靠性。一方面，应该鼓励军用软件研制单位积极参加第三方软件开发标准组织的评定，提高软件开发能力的提升；另外一方面，使用各种软件测试工具尽可能多地对软件的功能进行正确性测试，尤其是对关键和重要模块设计全覆盖的测试用例对其测试；同时，鼓励软件开发人员规范化设计文档，提高软件理论水平，使用各种软件分析与验证工具对软件的各种模型和代码进行验证和分析，尽可能早地发现软件的设计缺陷和错误。

［1］GJB 4072A-2006.军用软件质量监督要求［S］.北京：总装备部，2006.

［2］Leveson N G.Software Safety:Why，What，and How［J］. Computer Surveys，1986，18（2）：125-163.

［3］GJB 5000A-2008.军用软件研制能力成熟度模型［S］.北京：总装备部，2008.

［4］Paulk M C，Weber，C V，Curtis B et al.Capability Maturity Model for Software,Version 1.1［R］.Technical Report. CMU/SEI-93-TR-024 ESC-TR-93-177，1993.

［5］Pnueli A.The Temporal Logic of Programs［C］//Proc.of 18th IEEE Symposium on Foundation of Computer Science.IEEE Computer Society，1977，46-57.

［6］Emerson E A，Clarke E M.Characterizing Correctness Properties of Parallel Programs Using Fixpoints［C］//Proc.of the 7th Int.Colloquium of Automata,Languages and Programming，1980.

［7］袁崇义.Petri网原理与应用［M］.北京：电子工业出版社，2005.

［8］刘俊先，罗雪山.基于影像图方法的C4ISR作战模型［J］.系统工程与电子技术，2003，25（5）：537-539.

［9］张维明，邱涤洲.C3I系统理论基础：C3I系统建模方法与技术［M］.长沙：国防科技大学出版社，2000.

［10］贾子英，杨金照，闫飞龙.防控体系分布式指挥系统研究［J］.现代防御技术，2013，41（2）：118-122.

［11］朱涛，常国岑，施笑安.基于复杂网络的指挥信息系统拓扑模型研究［J］.系统仿真学报，2008，20（6）：1574-1576.

［12］King J C.Symbolic Execution and Program Testing［J］. Journal of the ACM，1976，19（7）：385-394.

［13］董龙明.基于域敏感内存抽象模型的堆操作程序静态分析［D］.长沙：国防科技大学，2012.

Static Analysis and Verification Technology for Reliability of Military Command and Control Software

XU Jing-Qi1,DONG Long-ming2,HAO Li-bo1
（1.Hunan Mechanical and Electrical Polytechnic,Changsha 410151，China；2.Nanjing Military Representative Office of The General Armament Department，Nanjing 210000，China）

With improving the informatization level of weapon equipment，the reliability of military command and control software is directly related to its overall effectiveness.On basis of the research of traditional software quality assurance technologies，the formal method based software analysis and verification technology are presented according to the characteristic of the military command and control software.It includes：the formal safety specification technology，the verification technology of the command software based on model checking and the analysis technology of the control software based on static analysis.In the end，the formal analysis and verification integrated environment suitable for the life cycle development of the command and control software are put forward.

military command and control software，analysis and verification technology，model checking，static analysis

TP39

A

1002-0640（2015）08-0176-05

2014-07-02

2014-08-07

湖南省科技厅应用基础研究项目（2014FJ3050）；湖南省教育科学规划基金资助项目（XJK013CXX003）

许婧棋（1983-），女，湖南常德人，硕士，讲师。研究方向：多目标算法与智能控制、软件工程。