摘要：测试用例的自动生成是验证安全苛求软件最关键的技术问题，然而目前的研究并没有充分考虑安全苛求软件的安全性需求，为此提出一种应用安全覆盖准则的安全苛求软件的测试用例自动生成策略，将该策略应用于铁路车站计算机连锁软件，并与全节点覆盖准则进行了比较。结果表明该策略对关键变迁有更高的安全性保证。
关键词：安全苛求软件； 测试用例自动生成； 安全覆盖准则
软件应用的日趋广泛， 加深了社会和经济对计算机的依赖，但软件故障时常会给人们的生活带来不便， 甚至不安。特别是一些软件， 其行为直接关系到人们的生命安全、大宗财产的损失和严重的环境破坏。这些软件就是通常所说的安全苛求软件。如何保障这些软件的质量，防止灾难性事故的出现，已成为一个刻不容缓的研究课题。
软件测试是软件生产中必不可少的质量保障手段。尤其是对于高可靠、高安全的安全苛求软件，更需要对它进行测试以尽可能多地发现程序中的缺陷。基于规格说明的测试从软件的规格说明推导测试用例。目前的研究主要对功能性需求规格进行建模，研究人员提出了各种覆盖准则覆盖状态图中的所有功能。然而对于安全苛求软件，仅仅覆盖软件功能是不充分的。因此本文提出了一种应用安全覆盖准则的安全苛求软件的测试用例生成策略：采用测试用例自动生成算法，生成覆盖所有节点、覆盖导致软件失效的关键变迁中防护函数的谓词公式的迁移序列，从而得到测试用例。
1、从形式规格说明产生测试用例的现状分析
软件的需求规格说明分为两类，即功能性需求规格和安全性需求规格。功能性需求规格常常注重各个构件所能完成的功能；安全性需求规格侧重各个构件之间的约束关系。以铁路连锁软件为例，它由信号机、道岔和区段这几个构件组成。
功能性需求规格体现了单个构件的功能，描述了系统的正确行为，如信号机的开放和关闭功能、道岔的转动和锁闭功能，以及区段的占用和锁闭功能。但是如果某一区段处于占用状态或道岔没有锁闭，这样的危险组合下建立进路可能会引发撞车、挤岔等严重事故，因此必须关闭信号机。安全需求规格就定义了这些构件之间的制约规则，并要求屏蔽那些危险组合，由故障导向安全。
目前从形式规格说明产生测试用例的方法都是针对软件的功能性需求规格进行建模，使用的覆盖准则只是考虑覆盖状态图中的所有节点或所有谓词公式。例如文献[2]利用基于有限状态机的经典测试U方法来自动生成测试输入序列，其测试序列覆盖每个状态迁移，当其测试覆盖准则仅仅是最基本的状态覆盖准则；文献 [3]根据UML状态图对被测试的对象行为或系统行为建模，然后按照不同的充分性测试准则分别生成测试用例，造成测试用例过于庞大，浪费了过多的时间和精力。
对于安全苛求软件的测试，关键是消除并控制软件出现危险或发生意外事故，所以上述方法考虑功能性需求是不充分的，必须对安全苛求软件的安全性需求规格进行建模。有色Petri网[4](colored Petri net，CPN)提供了一种精确的、一致的、易于被机器处理的符号来描述需求规格，相较于有限状态机和UML状态图，它简化了大型实际系统模型的复杂程度，更好地描述了模型的并发、冲突状况。与功能性需求建模不同的是，形式化安全性需求应该着重描述构件间的约束规则及系统发生失效的行为和结果。鉴于安全性需求和功能性需求的不同，测试用例的充分性不再体现在覆盖所有功能上，而是需要完全覆盖各种可能的失效情况，所以上述方法中的覆盖准则不再适用。本文在文献[3]和基本测试覆盖准则的基础上，提出了一种新的适用于安全苛求软件的测试覆盖准则——安全覆盖准则；然后采用有色Petri网形式化安全需求规格说明，根据此覆盖准则，通过测试用例自动生成算法生成覆盖所有库所和变迁的迁移序列，并在导致软件失效的关键变迁上对迁移序列进行全谓词公式覆盖扩展；最后从迁移序列得到测试用例。
2、安全覆盖准则
安全性需求的重要部分在于软件如何以安全的失效方法以及失效可以容许到何种程度的规范约束，因此适用于功能性需求规格的覆盖准则只考虑全面覆盖状态图中的所有节点是不足的，必须充分挖掘导致软件失效并引发严重事故的所有测试条件组合。根据以上思路，本文提出了安全覆盖准则。定义安全覆盖准则之前，先引入关键变迁的概念。
定义1 给定一个t，如果t(v=false)，则称t为关键变迁。其中：t表示Petri网模型中的变迁；v表示Petri网模型中的防护函数。
根据关键变迁的定义，可以看到它对应需求规格说明模型中存在判断且判断为假的部分，而在安全苛求软件中，它可能会引发或产生严重危害性事故。安全覆盖准则定义如下：
定义2 给定一个S，其满足条件：a)p∈P，pS；b)t∈T，tS；c)v∈V，(v∧v)S，则称S符合安全覆盖准则。其中：S表示测试用例集；p表示Petri网模型中的库所；t表示Petri网模型中的变迁；v表示Petri网模型中的防护函数。安全覆盖准则说明测试用例集应该使模型中的每一个库所至少被访问一次，每一个变迁至少被激活一次，且使Petri网模型中关键变迁的防护函数v的每一个主要谓词P取假各一次(次要谓词都为真)。防护函数的谓词公式中凡是要测试的谓词都应该分别充当一次主要谓词。对于一个主要谓词分别取假一次，将分别对应一个测试用例的产生。可见满足安全覆盖准则的这些测试用例遍历了模型中所有的节点，并且完全包含了可能导致危害性事故的变迁的各种谓词组合。
