一种嵌入式软件安全性自动化验证系统及其验证方法

权利要求

1.一种嵌入式软件安全性自动化验证系统，其特征在于：该系统包括：

A软件需求建模模块(1)，其功能是根据待验证软件的ICD文件和需求规格说明对待验证软件进行形式化描述，形成软件需求模型文件，该软件需求建模模块(1)包括：ICD建模模块(2)，其功能是描述待验证软件运行的外部交联环境，包括与外部设备之间的交联关系、总线类型及通信协议，形成ICD模型数据；

软件形式化建模模块(3)，其功能是在ICD模型数据的基础上，采用OCL形式化语言描述待验证软件的内部行为，包括状态迁移及功能逻辑，最终形成软件需求模型文件；

该软件需求建模模块(1)中，ICD建模模块(2)与软件形式化建模模块(3)连接，由ICD建模模块(2)向软件形式化建模模块(3)传输ICD模型数据；

B安全性验证规则数据库(4)，其功能是存储安全性验证规则，并提供查询、匹配、更新、维护的接口；

C形式化验证模块(5)，分别与软件需求建模模块(1)和安全性验证规则数据库(4)连接，由软件需求建模模块(1)向形式化验证模块(5)传输软件需求模型文件，由安全性验证规则数据库(4)向形式化验证模块(5)提供验证的依据，即安全性验证规则，该形式化验证模块(5)的功能是基于安全性验证规则数据库(4)中的安全性验证规则，对软件需求建模模块(1)形成的软件需求模型文件进行形式化验证，形成形式化验证结果；

D安全性测试模块(6)，分别与软件需求建模模块(1)、安全性验证规则数据库(4)和形式化验证模块(5)相连接，由软件需求建模模块(1)向安全性测试模块(6)提供软件需求模型文件，由安全性验证规则数据库(4)向安全性测试模块(6)提供安全性验证规则，由形式化验证模块(5)向安全性测试模块(6)提供形式化验证结果，该安全性测试模块(6)的功能是根据的软件需求模型文件和形式化验证结果以及安全性验证规则生成测试用例并通过翻译进行用例格式转换，以适应不同测试执行平台的需要，该安全性测试模块(6)包括：测试用例生成模块(7)，其功能是生成XML格式的测试用例；

测试用例翻译模块(8)，其功能接收测试用例生成模块(7)生成的XML格式的测试用例，并将其翻译成其它格式的测试用例，其它格式包括自然语言格式、脚本语言格式。

2.用于权利要求1所述嵌入式软件安全性自动化验证系统的验证方法，其特征在于：该方法的步骤如下：步骤一、通过对待验证软件运行的外部交联环境，包括与外部设备之间的交联关系、总线类型及通信协议的描述，建立ICD模型数据；

步骤二、在ICD模型数据的基础上，采用OCL形式化语言描述待验证软件的内部行为，包括状态迁移及功能逻辑，建立软件需求模型文件；

步骤三、将已有的软件失效原因，归纳形成安全性验证规则，建立安全性验证规则数据库；

步骤四、基于安全性验证规则数据库中的安全性验证规则，对软件需求模型文件进行形式化验证，获得形式化验证结果；

步骤五、根据软件需求模型文件、形式化验证结果以及安全性验证规则，生成XML格式的安全性测试用例；

步骤六、对XML格式的安全性测试用例进行格式转换，生成测试执行时所需要的用例格式。

说明书

一种嵌入式软件安全性自动化验证系统及其验证方法

技术领域

[0001] 本发明是一种嵌入式软件安全性自动化验证系统及其验证方法，属于软件安全性分析领域。

背景技术

[0002] 嵌入式软件在航空航天等领域广泛应用，越来越多的功能采用软件实现。近年来，随着软件复杂性的提高，软件失效导致的故障频繁发生，因此保障嵌入式软件的安全性已成为近年来软件工程领域的研究热点。欧美成熟经验表明，开展软件安全性分析工作是提升软件质量的有效方法，主要工作包括嵌入式软件安全需求的提取与规约、面向标准的嵌入式软件开发、嵌入式软件安全需求验证三部分内容。

[0003] 嵌入式软件需求验证是安全性分析中的关键环节，形式化验证和软件测试是嵌入式软件安全需求验证的主要方法。这两种方法各有利弊，形式化验证能够在软件需求分析和设计的早期阶段发现模型漏洞，缩短研发周期，且通过形式化验证能够挖掘由多个控制功能之间的数据交互、时序约束、并发组合等复杂逻辑关系引发的软件需求缺陷。但是形式化方法本身的复杂性对工程人员提出了很高的要求，使得当前在国内普及使用非常困难。此外，形式化验证的分析对象是软件模型，无法发现软件模型与具体实现不一致而导致的软件缺陷。在国内，软件测试仍然是提高对软件安全性的最有效的手段，软件测试通常在研制的中后期开展，被测软件被安装在真实的硬件设备中运行，不仅能找出代码实现的局部方法错误等细枝末节问题，还能找出由于软件实现与模型在逻辑上的背离而导致的重大安全性问题。但软件测试过程中由于测试用例的覆盖率有限，难以穷尽对整个系统的测试，而安全苛求系统的运行通常与外部环境有关，其执行往往具有不确定性，测试极为困难，因此软件测试方法不能从根本上保证系统的安全性。

[0004] 目前，形式化验证方法由于理论性较强，在嵌入式软件研制过程中较少开展。而对于软件测试，虽然有部分测试平台出现，但普及程度较低。大多采用人工测试的方式，对于复杂的软件系统，测试效率低，并且无法发现多状态并发、多功能冲突等导致的软件问题。

发明内容

[0005] 本发明正是针对上述现有技术领域中存在的不足而设计提供了一种嵌入式软件安全性自动化验证系统及其验证方法，其目的是根据形式化验证和软件测试的特点和互补性，将这两种技术手段相融合，结合国内工程实际和研制要求，综合考虑分析要素和工程限制，提出一种符合国内研制现状的种嵌入式软件安全性自动化验证系统及其验证方法，提高国内嵌入式软件需求验证水平。

[0006] 本发明的目的是通过以下技术方案来实现的：

[0007] 本发明技术方案提出了一种嵌入式软件安全性自动化验证系统，其特征在于：该系统包括：

[0008] A软件需求建模模块(1)，其功能是根据待验证软件的ICD文件和需求规格说明对待验证软件进行形式化描述，形成软件需求模型文件，该软件需求建模模块(1)包括：

[0009] ICD建模模块(2)，其功能是描述待验证软件运行的外部交联环境，包括与外部设备之间的交联关系、总线类型及通信协议，形成ICD模型数据；

[0010] 软件形式化建模模块(3)，其功能是在ICD模型数据的基础上，采用UML和OCL形式化语言描述待验证软件的内部行为，包括状态迁移及功能逻辑，最终形成软件需求模型文件；

[0011] 该软件需求建模模块(1)中，ICD建模模块(2)与软件形式化建模模块(3)连接，由ICD建模模块(2)向软件形式化建模模块(3)传输ICD模型数据；

[0012] B安全性验证规则数据库(4)，其功能是存储安全性验证规则，并提供查询、匹配、更新、维护的接口；

[0013] C形式化验证模块(5)，分别与软件需求建模模块(1)和安全性验证规则数据库(4)连接，由软件需求建模模块(1)向形式化验证模块(5)传输软件需求模型文件，由安全性验证规则数据库(4)向形式化验证模块(5)提供验证的依据，即安全性验证规则，该形式化验证模块(5)的功能是基于安全性验证规则数据库(4)中的安全性验证规则，对软件需求建模模块(1)形成的软件需求模型文件进行形式化验证，形成形式化验证结果；

[0014] D安全性测试模块(6)，分别与软件需求建模模块(1)、安全性验证规则数据库(4)和形式化验证模块(5)相连接，由软件需求建模模块(1)向安全性测试模块(6)提供软件需求模型文件，由安全性验证规则数据库(4)向安全性测试模块(6)提供安全性验证规则，由形式化验证模块(5)向安全性测试模块(6)提供形式化验证结果，该安全性测试模块(6)的功能是根据的软件需求模型文件和形式化验证结果以及安全性验证规则生成测试用例并通过翻译进行用例格式转换，以适应不同测试执行平台的需要，该安全性测试模块(6)包括：

[0015] 测试用例生成模块(7)，其功能是生成XML格式的测试用例；

[0016] 测试用例翻译模块(8)，其功能接收测试用例生成模块(7)生成的XML格式的测试用例，并将其翻译成其它格式的测试用例，其它格式包括自然语言格式、脚本语言格式。

[0017] 本发明技术方案还提出用于上述嵌入式软件安全性自动化验证系统的验证方法，其特征在于：该方法的步骤如下：

[0018] 步骤一、通过对待验证软件运行的外部交联环境，包括与外部设备之间的交联关系、总线类型及通信协议的描述，建立ICD模型数据；

[0019] 步骤二、在ICD模型数据的基础上，采用OCL形式化语言描述待验证软件的内部行为，包括状态迁移及功能逻辑，建立软件需求模型文件；

[0020] 步骤三、将已有的软件失效原因，归纳形成安全性验证规则，建立安全性验证规则数据库；步骤四、基于安全性验证规则数据库中的安全性验证规则，对软件需求模型文件进行形式化验证，获得形式化验证结果；

[0021] 步骤五、根据软件需求模型文件、形式化验证结果以及安全性验证规则，生成XML格式的安全性测试用例；

[0022] 步骤六、对XML格式的安全性测试用例进行格式转换，生成测试执行时所需要的用例格式。

[0023] 本发明的优点与积极效果在于：

[0024] (1)采用本发明技术方案构建的安全性自动化验证系统，结合了形式化验证和软件测试两种方法，实现了在研制早期对软件需求模型进行形式化验证，在研制中后期，为软件测试提供了测试用例，弥补了现有单一方法的不足，增强了验证的充分性；

[0025] (2)采用本发明技术方案构建的安全性自动化验证系统大大降低了用户的使用门槛，易于推广，软件需求建模模块中采用的UML和OCL形式化语言是相关领域从业人员普遍掌握的技术，验证系统的适用人员无需掌握复杂的形式化验证算法；

[0026] (3)采用本发明技术方案构建的安全性自动化验证系统实现了形式化验证和安全性测试用例生成的自动化，用户只需构建软件需求模型文件和选择采用的安全性验证规则，验证工作由系统自动完成；

[0027] (4)本发明技术方案构建的安全性自动化验证系统中安全性验证规则数据库的提出，为工程经验的积累及使用提供了切实可行的方法，有利于建立具有自主知识产权的领域失效数据库，通过经验数据的不断积累，对后期研制的指导作用不断增强；

[0028] (5)本发明技术方案构建的安全性自动化验证系统降低了工程实施难度，对复杂的发控软件进行建模时取得良好效果；

[0029] (6)本发明技术方案构建的安全性自动化验证系统基于安全性验证规则的形式化验证更有针对性，避免使用穷举遍历的方法导致的空间爆炸问题；

[0030] (7)本发明技术方案构建的安全性自动化验证系统获得的形式化验证结果预置条件明确，输入数值精准，可操作、可实施，便于发现问题时人工复现及回放；

[0031] (8)本发明技术方案构建的安全性自动化验证系统建模时采用标准的UML建模语言，符合相关国军标标准，构建的模型可以直接用于软件需求分析及设计中，避免了多次重复建模；

[0032] (9)本发明技术方案构建的安全性自动化验证系统在需求建模时采用了相同的建模元素，形式化验证和安全性测试的对象是具有统一格式的软件需求模型，所以能够编写通用的形式化验证算法和测试用例生成算法，因此该方法能够应用于各领域嵌入式软件安全性验证中，具有很好的通用性。

附图说明

[0033] 图1是本发明技术方案构建的安全性自动化验证系统的框图

[0034] 图2是本发明技术方案中软件需求建模模块构建流程图

[0035] 图3是本发明技术方案中软件外部交联环境及接口示意图

[0036] 图4是本发明技术方案中状态图基于OCL的形式化描述示例

[0037] 图5是本发明技术方案中安全性验证规则数据库的形成和使用过程[0038] 图6是本发明技术方案中基于安全性验证规则的模型检测算法示例[0039] 图7是本发明技术方案中状态功能关联后的需求模型示例

具体实施方式

[0040] 以下将结合附图和实施例对本发明技术方案作进一步地详述：

[0041] 参见附图1所示，本发明技术方案所述的嵌入式软件安全性自动化验证系统，其特征在于：该系统包括：

[0042] A软件需求建模模块1，其功能是根据待验证软件的ICD文件和需求规格说明对待验证软件进行形式化描述，形成软件需求模型文件，该软件需求建模模块1包括：

[0043] ICD建模模块2，其功能是描述待验证软件运行的外部交联环境，包括与外部设备之间的交联关系、总线类型及通信协议，形成ICD模型数据；

[0044] 软件形式化建模模块3，其功能是在ICD模型数据的基础上，采用OCL形式化语言描述待验证软件的内部行为，包括状态迁移及功能逻辑，最终形成软件需求模型文件；

[0045] 该软件需求建模模块1中，ICD建模模块2与软件形式化建模模块3连接，由ICD建模模块2向软件形式化建模模块3传输ICD模型数据；

[0046] 参见附图2所示，软件需求建模模块1是基于SafeTrip的建模工具通过以下步骤来实现的，其中：

[0047] ICD建模模块2的建模步骤为：

[0048] 1.如图3所示，以航空发动机控制软件为例，构建外部交联环境模型，具体过程如下：

[0049] 1.1使用建模工具，绘制待验证软件所在系统以及与之相连的系统，；

[0050] 1.2根据ICD文件使用总线连接待测软件所在系统与其他系统；

[0051] 1.3配制总线的接口信息，接口信息包括两部分：一部分是接口通信信息，即外部交联接口模型针对软件与外部交联设备之间的各种常见接口类型(例如ARINC 429，CAN，离散量、模拟量等)的通讯格式与内容，主要包括接口名称、接口类型、总线通信所需的波特率、路由寻址、优先级、传输速率等。另一部分是输入输出接口的约束条件。根据软件需求文档，明确各接口自身及相互之间的逻辑、时序约束条件。逻辑条件主要包括与、或、非、互斥等。时序条件包括前序、后序、并发、延时、计时等。

[0052] 2构建总线传输数据模型，具体过程如下：

[0053] 在外部交联环境模型的基础上，将总线数据拆分成数据帧和帧变量。并详细描述数据帧和帧变量的属性。总线数据包含一个或多个数据帧、数据帧具有传输方向，传输周期、数据帧长度等属性。每个数据帧包含多个帧变量，帧变量具有变量类型(整型、浮点型、字符型等)、长度等属性。

[0054] 软件形式化建模模块3的建模步骤为：

[0055] 1.构建内部数据元素和接口数据元素

[0056] 接口数据元素和内部数据元素是软件内部可识别的具有物理意义的变量，如高度、速度、油门杆角度，是后续功能模型和状态转移模型的操作对象，变量属性包含描述物理意义的信息，如数据单位、分辨率、误差、有效区间，接口数据元素描述了软件的对外交互行为，通过总线传输数据模型映射获得，如数据帧中的前两个short类型的帧变量可以映射成表示高度的Height接口数据元素,映射表达式为：Height＝Var1<<8+Var2。这里的映射表示的是值的映射，映射关系采用数学表达式，实现时可采用MuParser等工具以支持基于复杂运算的映射和解析，除了完成值的映射，接口数据元素获得了数据帧的周期等逻辑和时序信息，并将这些信息引入软件内部模型中，内部数据元素由软件内部处理时的中间结果和临时变量构成，从需求文档中获得；

[0057] 构建接口数据元素和内部数据元素的方式为：在SafeTrip工具中选择新建相应元素，然后配置元素的数据单位、分辨率、误差、有效区间，接下来配置该数据元素关联的数据帧变量，并使用MuParser表达式描述数据元素与帧变量的对应关系。

[0058] 2.参见附图4所示，基于UML状态图和OCL的形式化状态迁移模型

[0059] 有了接口数据元素和内部数据元素，可以采用标准UML中的状态图对软件运行的状态与方式进行建模，构建状态迁移模型，为了进行安全性分析，需要采用OCL对象约束语言对状态图中的状态转移进行形式化描述，标准UML中，状态转移的语法格式为：事件名[警戒条件]/动作表达式^发送子句，OCL对状态图的形式化扩展主要包括以下几方面：

[0060] 变化事件。变化事件是指如果一个布尔表达式中的变量发生变化，使得该表达式的值相应地变化，从而满足某些条件的事件。与警戒条件不同，当事件发生时，警戒条件只计算一次，如果条件为假，状态转移将不会发生。当变化事件发生时，警戒条件可能阻塞，等待警戒条件满足后进行状态迁移；

[0061] 警戒条件。OCL表达式可以用于状态警戒条件的描述，描述位置为触发转移发生的事件之后的方括号内；

[0062] 动作表达式实参。状态图中的动作包含操作的调用和发送事件，通常需要携带参数，为了满足安全性分析的需要，此处参数需要明确指定实参，而不能使用形参。此时，需要使用OCL表达式明确指定实参；

[0063] 发送子句。状态图迁移动作表达式指出了当状态转移被激活时(对象状态发生转移时)，对象本身需要执行的动作。有时对象能自己执行所有的功能，需要其它对象的帮助，从而对象就需要发送消息给其它对象。此时需要利用发送子句。而OCL可以用于描述发送子句的目标对象；

[0064] 3.功能层次模型

[0065] 对软件运行的状态进行建模以后，开始进行功能分解，构建软件功能层次模型。以发动机中数字电子控制系统核心机软件为例，软件功能可以分解为发动机控制和故障监控功能，发动机控制功能可以进一步分解为燃油控制、导叶控制、开关控制。而故障监控功能可以分解为信号自检、回路监控和消喘功能；

[0066] 使用SafeTrip建模工具构建功能层次模型时，在功能层次建模模块中，逐个添加功能分解获得的功能模块，为每个功能模块添加名称、功能标识。然后使用连接线连接父功能和子功能，连接方向为由父功能指向子功能。

[0067] 4.建立状态功能关联

[0068] 功能分解完成后，需要建立功能与状态的关联关系，分解后的功能与状态是多对多的关系，同一状态中可能有多个功能并发执行，同一功能可能出现在多个不同的状态中，进行功能状态关联后，允许检查功能状态组合等复杂逻辑特性引发的软件失效。功能与状态的关联关系在软件需求规格说明中描述，其中，要求的状态和方式描述了软件运行时的状态，CSCI能力需求描述了与状态对应的各个功能。SafeTrip提供了由状态关联功能和由功能关联状态两种方式，具体构建时按照软件需求规格说明描述的关联关系，通过鼠标右键点击状态关联软件功能，也可以右键点击功能关联软件状态。

[0069] 5.基于UML操作图和OCL的形式化功能模型

[0070] 采用UML和OCL对象约束语言对软件功能进行建模，实现对软件内部处理流程的形式化描述。为了进行安全性分析，将功能模型拆分为软件外部输入接口(Input)-功能处理过程(Process)-外部输出接口(Output)(简写为IPO)这三项需求元素，构成了软件运行时的动态失效链。失效链中的任何一个环节(即外部输入接口、功能处理过程、外部输出接口)出现故障，经过失效链的传递，最终都有可能导致软件发生失效，进而对系统产生影响。

[0071] 功能的外部输入接口和外部输出接口从接口数据元素和内部数据元素中选取并进行关联。功能处理过程采用UML中的活动图表示，与状态迁移模型中的状态图类似，采用OCL对象约束语言对活动图进行扩展：

[0072] 指定对象实例。使用OCL表达式指定执行某一活动的对象实例，使用方法类似于状态中的发送子句中的目标对象；

[0073] 决策条件和同步条件描述。使用方法类似于上文状态图中警戒条件；

[0074] 指定实际参数。使用方法与状态图类似。

[0075] B安全性验证规则数据库4，其功能是存储安全性验证规则，并提供查询、匹配、更新、维护的接口；

[0076] 安全性验证规则数据库4的构建方式参照图5所示：

[0077] 首先，需要搜集失效数据，数据来源主要包括型号软件安全性分析项目中发现的软件失效模式；软件自测试、第三方测试、型号鉴定测评、定型测评过程中发现的软件问题；在进行软件测试过程中，与软件开发人员交流时获取的研制过程中发现的需求缺陷；以及其他可获取的事故案例数据，如外场试飞过程发现的问题，已经发生的相关领域的典型事故案例(德国汉莎航空公司空难、美国火星探测器坠毁等)。

[0078] 获取失效数据后，需要进行分析以找到引发问题的失效原因。接下来，以联合航空751号班机空难为例，阐述获取安全性验证规则的过程。此次空难原因是起飞前除冰不彻底，飞机积冰脱落导致引擎喘振，飞行员试图减小油门从而减小引擎喘振，但飞机上装有的自动推力恢复系统，反而使推力增大加剧了事故严重程度。获取失效现象后，首先需要对失效原因进行总结归纳，挖掘失效原因中蕴含的深层次失效机理，使得最终形成的安全性验证规则能够应用到各类型软件的安全性需求分析工作中。经过分析发现，问题的深层次原因是系统重启状态中的多个功能对同一个变量赋予不同的值，导致赋值冲突。接下来，对该失效机理进一步扩展，根据UML状态图可知，状态图中可以存在并发状态，多个并发状态中可能出现多个功能对同一个变量出现赋值冲突的情况，赋值冲突由单个状态扩展到整个系统运行时的多个并发状态。最终获得如下安全性验证规则：“整个系统运行过程中，存在多个功能同时对一个变量进行输出，导致赋值冲突”。使用上述方法积累安全性验证规则，其中部分规则如下：输入接口数据元素的取值为有效区间外的异常值、输出接口数据元素输出数据速率大于总线传输速率、功能处理未覆盖输入接口数据元素的整个有效区间、同一个状态的多个迁出条件同时满足、状态多个迁出转移条件未覆盖条件变量的完整的取值区间、状态图中存在不可达状态、状态图中迁移前状态和迁移后状态对同一个变量赋予不同的值等。上述安全性验证规则中所蕴含的失效可能引发系统危险，是后续开展模型检测和安全性测试的依据。

[0079] 为了便于数据库查询、匹配、更新和维护，将分析得到的安全性验证规则进行分类：分别是功能输入接口失效、功能输出接口失效、独立功能失效、组合功能失效、状态失效等。最终形成了安全性验证规则数据库。同时，可以根据需要对所分析的业务领域中的对象，构建系统层次树，如飞机系统可以分为导航系统、飞控系统、液压系统等，每个系统又可以进一步分为子系统。最终，可以将安全性验证规则与具体的系统关联，以便于查询使用。

[0080] C形式化验证模块5，分别与软件需求建模模块1和安全性验证规则数据库4连接，由软件需求建模模块1向形式化验证模块5传输软件需求模型文件，由安全性验证规则数据库4向形式化验证模块5提供验证的依据，即安全性验证规则，该形式化验证模块5的功能是基于安全性验证规则数据库4中的安全性验证规则，对软件需求建模模块1形成的软件需求模型文件进行形式化验证，形成形式化验证结果；

[0081] 形式化验证模块5的构建方式如下：

[0082] 软件安全性自动分析的实现过程是针对每条安全性验证规则的语义，使用计算机程序编写一个模型检测算法。模型检测算法根据安全性验证规则的语义对需求模型进行遍历，算法依据时序关系、判断条件、转移条件、取值有效区间等信息，对复杂的软件需求模型进行静态扫描，找出安全性验证规则中指定的所有可能引发系统危险的失效模式；

[0083] 需求模型构建过程中，对不同软件内外部行为描述的方法是一致的，所获得的模型是采用的建模元素构建的无歧义的形式化模型。安全性验证规则获取的过程中，获得的每条规则采用独立的标识，分析规则的语义也是无歧义的。以上两点确保了实现模型检测算法的可行性和算法的通用性；

[0084] 接下来，以“整个系统运行过程中，存在多个功能同时对一个变量进行输出，导致赋值冲突”分析规则为例，给出模型检测算法的实现方法描述以及实现算法的伪代码；

[0085] 模型检测算法描述：

[0086] 第一步，通过遍历状态模型，找到系统中并发的状态，系统中可能存在多组并发状态，需要对每一组施加以下算法；

[0087] 第二步，通过需求模型中的状态功能关联关系，遍历出每个状态下同时运行的功能；

[0088] 第三步，通过功能模型，找到每个功能的输入输出接口数据元素；

[0089] 第四步，检查是否存在多个功能具有相同的输出接口数据元素；

[0090] 第五步，对具有相同输出接口数据元素的功能，检查对输出接口数据元素的赋值操作是否可能同时发生。即检查多个功能模型中，从活动图起点到接口赋值操作所在活动的路径上的决策条件是否可能同时发生。伪代码如附图6所示。

[0091] 在模型检测过程中，需要对发现软件失效的安全性验证规则以及产生失效的状态和功能进行存储，安全性测试用例生成时需要根据这些安全性验证规则需要生成有针对性的测试用例，进一步确认模型是否进行了有效修改，避免失效的出现。

[0092] D安全性测试模块(6)，分别与软件需求建模模块1、安全性验证规则数据库4和形式化验证模块5相连接，由软件需求建模模块1向安全性测试模块(6)提供软件需求模型文件，由安全性验证规则数据库4向安全性测试模块(6)提供安全性验证规则，由形式化验证模块5向安全性测试模块(6)提供形式化验证结果，该安全性测试模块(6)的功能是根据的软件需求模型文件和形式化验证结果以及安全性验证规则生成测试用例并通过翻译进行用例格式转换，以适应不同测试执行平台的需要，该安全性测试模块(6)包括：

[0093] 测试用例生成模块(7)，其功能是生成XML格式的测试用例；

[0094] 测试用例翻译模块(8)，其功能接收测试用例生成模块(7)生成的XML格式的测试用例，并将其翻译成其它格式的测试用例，其它格式包括自然语言格式、脚本语言格式。

[0095] 测试用例生成模块(7)的实现方式为：

[0096] 根据上文的需求建模过程可以看出，本发明技术方案构建的安全性自动化验证系统采用状态图描述系统生命周期，表现系统所具有的各种状态和状态迁移，以及影响系统状态的事件，主要描述了系统从一个状态到另一个状态变化迁移的控制流。每个状态中的业务逻辑采用活动图进行描述，一个状态中可能存在多个功能，而状态图可以分为区域，而区域又包括退出或者当前执行的子状态。说明组合状态在某一时刻可以同时达到多个子状态。将状态和功能进行关联后，形成的最终的模型图。附图7是一个简单的需求模型图，首先，使用状态图描述了系统各个状态，包括状态1和状态2，其中，状态1是一个组合状态，包含两个并发的子状态，分别是状态1-1和状态1-2。其中，每个状态关联一个或多个使用活动图描述的功能，图中状态1-1关联了功能1和功能2，状态1-2关联了功能3，状态2关联了功能4。

[0097] 生成安全性测试用例时，结合了基于状态图和活动图的测试用例方法，安全性测试用例包括两类，分别是通用的安全性测试用例和基于安全性验证规则的有针对的安全性测试用例。

[0098] 通用安全性测试用例的生成方法：首先，进行状态测试时，采用基于状态图生成方法，首先将具有层次结构的状态图转换为单层状态图，然后使用广度优先遍历算法遍历整个状态图，确保每个状态被遍历，这样生成了多个测试场景。每个状态可以作为一个测试场景，状态中关联的多个功能的活动图表示此场景的所有的被测的操作序列。每个功能的操作序列就是一个测试案例。接下来采用基于活动图的测试用例生成方法，生成安全性测试用例。使用上述方法生成了通用的安全性测试用例。

[0099] 基于安全性验证规则的安全性测试用例生成方法：首先，步骤三中在进行模型检测时，存储了引发软件失效的安全性验证规则以及所在的状态及功能。生成用例时，首先构造预置条件到达目标状态，然后根据安全性验证规则的含义，遍历活动图产生测试用例。

[0100] 测试用例翻译模块(8)的实现方式为：

[0101] 通过安全性测试用例生成模块，生成了XML格式的测试用例，安全性用例翻译模块的工作主要是进行格式替换。状态迁移模型和活动图中迁移条件均采用接口数据元素和内部数据元素进行描述。因而，生成的XML格式用例中的操作对象也是接口数据元素和内部数据元素。由于在需求建模时每个接口数据元素和内部数据元素都有两类名称，分别是人工可识别的变量名和英文变量名，且英文变量名符合脚本语言变量命名规范。这就为用例格式转换提供可可行的方案。测试用例包含多个步骤，每个步骤包含两个核心要素，分别是操作时间和此时刻对变量的操作。安全性用例翻译模块的工作是按照目标格式的要求，对XML用例中的时间和变量操作进行格式替换。翻译成人工执行的用例时，将变量名替换为人工可识别的变量名，翻译成测试脚本格式的用例时，将变量名替换为英文变量名。翻译成其它格式的XML用例时，保留原变量名，对用例格式重新进行组织即可。

[0102] 上述嵌入式软件安全性自动化验证系统的验证方法的步骤如下：

[0103] SafeTrip建模工具、形式化验证模块以及安全性测试模块安装部署在同一台Windows 7系统的PC上，安全性验证规则数据库实现时采用Oracle数据库，部署在单独的数据服务器上，PC与数据服务器采用网线连接。

[0104] 步骤一、打开PC机的SafeTrip建模软件，根据上文所述的ICD建模步骤，构建ICD模型，形成ICD模型数据；

[0105] 步骤二、在ICD模型数据的基础上，采用OCL形式化语言描述待验证软件的内部行为，包括状态迁移及功能逻辑，建立软件需求模型文件；

[0106] 步骤三、打开数据服务器，将已有的软件失效原因，归纳形成安全性验证规则，存放在Oracle数据库中；

[0107] 步骤四、在形式化验证模块中，导入软件需求模型文件和Oracle数据库中的安全性验证规则，对软件需求模型文件进行形式化验证，获得形式化验证结果；

[0108] 步骤五、打开测试用例生成模块，导入软件需求模型文件、形式化验证结果以及Oracle数据库中的安全性验证规则，生成XML格式的安全性测试用例；

[0109] 步骤六、对XML格式的安全性测试用例进行格式转换，生成测试执行时所需要的用例格式。包括人工执行所需要的自然语言用例、基于测试脚本的测试工具平台所需要的脚本语言格式用例、嵌入式仿真自动化测试平台需要的其他XML格式用例以及其他的格式用例。

[0110] 步骤七、执行步骤六中生成的测试用例，对被验证软件进行软件测试。