随着计算系统的功能、结构、规模日趋庞大而复杂,系统是否可信已成为当前非常关注的问题^[1].可信是指系统的行为及其结果是可预期的、行为状态是可监测的、行为结果是可评估的、行为异常是可控的^{[2, 3]}.安全苛刻系统(safety critical system,简称SCS)对可信性的需求典型而迫切,其系统功能一旦失效将引起财产、生命的重大损失以及环境可能遭到严重破坏.它广泛存在于航空航天、交通运输等领域.近年来,这类重大事故屡见不鲜,因而研究评估和验证安全苛刻系统的可信性具有现实意义.安全苛刻系统的可信性一般是通过测试来支持,因而获取准确可靠的测试结果数据至关重要.然而安全苛刻系统一般是复杂系统,人工测试方式一方面给测试带来不准确性,另一方面,很多测试也无法用人工方式进行,因此,测试的信息化和自动化已成为安全苛刻系统测试发展的主要趋势.自动化测试包括测试用例自动生成和测试过程的自动化,本文以测试过程的自动化为主要内容展开研究.关于具体的测试方法、技术和理论等则不在本文的讨论范畴中.

测试语言是实现测试过程信息化和自动化的根本途径,国内外针对安全苛刻系统测试分别设计和开发了不同的测试语言或测试脚本语言.如美国宇航局NASA的GOAL^[4]、欧洲宇航局ESA的ETOL^[5]、ISYS公司发布的STOL^[6]、国际标准化组织IEEE的ATLAS^[7]、以色列Technion大学的T++^[8]、德国Tech S. A. T公司的航天系统测试脚本语言ADS2^[9].国内也展开广泛的研究,中国科学院光电研究院的ATLMIC^[10]、中国科学院空间科学与应用研究中心的卫星测试操作语言^[11]、同济大学用于高速铁路仿真测试的SED_SCS_STL^[12]、北京航空航天大学用于航天器测试的CATOL^[13]等.这些有代表性的测试语言在自动化测试中发挥了重要作用.

安全苛刻系统的测试是由测试人员借助测试设备完成对被测产品的测试.根据被测产品的需求描述设计测试任务,驱动测试设备对被测产品进行测试,通过判读获取的测试数据完成测试,如图 1所示.与以往相比,当前安全苛刻系统的测试面向新的测试需求,被测产品批量化生产网络并行测试对测试提出了更高的测试需求和更安全的可靠要求.同时,由于安全苛刻系统的特殊性和复杂性,其现有测试模型是在当时的技术环境下开发的,自动化程度低,硬件设备的耦合度高,开放性差,分系统之间融合度低,升级困难,很难满足新的测试需求.因此,由于安全苛刻系统领域的特殊性,需要深入分析和研究安全苛刻系统自动化测试过程中的相关理论、方法和技术,支持安全苛刻系统的自动化测试.

安全苛刻系统的自动化测试是通过测试任务、测试设备和被测产品三端交互协同完成的测试过程,包括这三端内部以及之间的交互协同.由于被测产品和测试设备的物理实体都是仪器和仪表等硬件设备,而这些硬件设备本身都是复杂系统,属于高阶对象,并且这些设备之间的交互需要通过传送设备操作指令(高阶数据)完成.另一方面,测试任务是通过测试设备访问被测产品,其中交互内容也主要是关于设备操作指令的高阶数据,因此,在安全苛刻系统自动化测试的协同过程中就表现出了交互内容和交互过程的高阶性,即协同对象和协同行为均具有高阶性.

为掌握实时的信息数据,安全苛刻系统一般具有实时性,测试中系统各部件之间不仅通过交互描述与功能相关的信息,而且还需要表达出时间方面的控制特征,并且由于系统部件之间的实时影响,测试任务上的控制结构与传统程序设计语言的控制结构的执行机制不同.

在安全苛刻系统测试中,被测产品状态参数在不同时刻具有不同值,以表征其不同的状态.不仅如此,被测产品状态参数的这些不同的取值在不同的时刻具有不同的参照关系,用于验证功能部件是否满足给定的功能.因此,安全苛刻系统的自动化测试过程具有时序性.

因此,安全苛刻系统的自动化测试过程呈现出上述的高阶协同性、实时性、时序性等特点,并且这些特性纠结在一起贯穿在整个自动化测试过程中,从而使得对安全苛刻系统测试过程中的测试行为难以进行准确地刻画与分析,造成测试过程自动化困难.

近年来,作者参与了安全苛刻系统(包括卫星、飞船、大型武器装备任务系统)的自动化测试和评估验证等方面的大量实际项目工作,积累了一定的实际工作经验.针对上述问题,采用形式化方法为安全苛刻系统的自动化测试建立形式化模型,精确描述和定义安全苛刻系统的自动化测试过程.以此为基础,提出用于安全苛刻系统自动化测试的测试语言,设计实现的相关自动化测试系统和平台已运行于实际应用中,取得了很好的效果.

1 相关工作

不同的形式化方法在描述能力、应用领域等方面有不同的侧重.目前,已有的形式化模型分别刻画了高阶、实时、时序等特性中的部分特性.如:刻画高阶性的典型工作有高阶CCS演算^[14]、高阶p演算^[15]、高阶并发通信模型^[16]、Ambient演算^[17]等;刻画实时性的有时间CSP模型^[18]、时间自动机^[19]、时段演算^[20]等;刻画时序性的有分支时态逻辑CTL^[21]、线性时态逻辑LTL^[22]、m演算逻辑^[23]等;刻画高阶和实时性的高阶实时演算模型时间p演算模型^{[24, 25]},高阶多型p演算THOp-calculus^[26]、高阶时段演算^[27];刻画实时和时序性的实时时序模型E-LOTOS^{[28, 29]}和XYZ/E^[30]等.本文主要讨论高阶协同性问题,故相关工作以高阶性模型展开论述.

在描述高阶性的模型中,由于并发模型中比较经典的模型有CCS模型^[31]和p演算模型^[32],目前的高阶演算模型主要是在二者的基础上扩展高阶定义,实现模型的高阶性.高阶CCS演算模型中,典型的有Thomsen的高阶通信系统演算CHOCS^[33]和PlainCHOCS^[34],二者均通过对CCS进行高阶通信扩展,即进程本身可以传递实现高阶定义,且这两个模型中没有一阶通信.CHOCS和PlainCHOCS之间的不同在于:CHOCS使用动态绑定,而PlainCHOCS使用静态绑定.

Sangiorgi在Thomsen的工作基础上对p演算进行扩展,其中任意阶的进程都可以被传送.它将高阶与一阶区别开来的同时也带来了一些复杂性,该演算模型称为高阶p演算^[15].

李未的并发演算CC^[16]是一种高阶并发通信系统的数学模型,把l演算作为子理论并包含一阶通信系统演算CCS、移动进程演算CMP、高阶通信系统演算CHOCS的主要特征.在CC中,通信端口可为任意表达式,并且进程和通信端口都可以作为通信中传递的一阶对象.从而使CC不仅可以描述高阶通信行为而且还可以刻画通信网络的动态自修改行为.

Ambient演算^[17]作为一种描述移动并发的模型,其高阶性体现在通过移动动作实现进程的移动.在Ambient演算中,分布计算节点被描述为一个叫做ambient的封闭结构,通过在ambient中定义的3种基本动作in,out, open实现ambient的移动,描述移动计算过程.Ambient演算是第一个成功地描述广域计算和移动计算的异步、高阶、并发演算,可看作是具有层次性、位置可移动和资源访问控制的p演算.

为了描述实时性,现有工作主要是在高阶模型上扩展实时性,以刻画系统行为与时间的关系.如:Degano等人^[24]对p演算的标号迁移系统LTS中的标号进行时间扩展,增加动作的完成时间信息和时间代价函数,定义了一种非时间良构的紧急同步的p演算时间操作语义.在该模型中,时间因素实际上被作为系统的一种特征属性信息而进行刻画;Berger^[25]在p演算的基本语法中扩展计时器结构,用以描述时间与动作的关联关系.以整数表示时间,用时间步骤函数静态离散描述动作的执行过程.西北工业大学尤涛等人^[26]以时态逻辑为基础,提出一种有时间特性的高阶多型p演算(THOp-calculus),其细化定义时间种类,实现系统行为与时间的关联.该模型主要应用于构件式实时软件的建模与演化分析;中国科学院软件研究所詹乃军^[27]用时段演算来刻画程序的实时行为.用高阶的时间函数来表示程序变量,建立高阶时段演算分析程序的实时性质.

在安全苛刻系统中,由于被测产品一般为复杂系统,在进行测试时需分级进行测试.为了支持测试模型的通用性,定义了一种独立于测试设备和被测产品的基本测试单元,称为测试原子.测试原子抽取和封装了基本的测试方法,在测试过程中具有可重用性和实时性的特点.测试任务即由这些测试原子组成.同时,被测产品和测试设备自身也是独立系统,这些系统进行交互完成测试的同时,内部既要根据交互信息,选择执行不同的操作来执行,又同时运行着其内部常规程序,并维护自身的状态;而且这些系统对外的接口具有不同的协议约束,并分别隶属于不同的应用域内,例如加电设备、计量设备等由相关的设备组成的设备应用系统.因此,无论是测试任务还是被测产品、测试设备,采用传统进程形式来描述将极其繁琐并给实现带来极大的不便.

现有高阶演算模型中,高阶性主要体现在进程自身可以当做一阶值进行传递.由于高阶进程可以被传递,其副作用也使进程间的交互关系发生变化,带来进程执行次序和进程间交互关系的不确定性,这些不确定性难以通过静态方法进行分析和验证.而在安全苛刻系统测试中,由于安全可靠至关重要,这些不确定因素会给测试带来安全隐患.因此,上述基于进程的分布式模型用于描述设备协同过程时存在着不足,但Ambient演算作为一种描述移动并发的模型,其ambient封装结构值得借鉴.

2 安全苛刻系统自动化测试中的高阶协同性

协同是多个资源实体间通过信息交互协调一致完成某个功能或目标的过程.若定义E为资源实体域,D为资源实体上的交互消息域,R为系统输出(运行结果)域,则一个协同系统可以定义为.一般协同系统中,D为一阶论域,即交互消息为一阶数据.当交互消息域为高阶域时,我们将这样的协同系统称为高阶协同系统.

在安全苛刻系统的测试中,被测产品和测试设备操作指令作为高阶对象操作密集出现,是测试系统测试行为交互的主要内容.而在安全苛刻系统测试过程中,协同涉及测试任务、测试设备以及被测产品三端之间的协同,为支持系统的开放性,测试设备可以动态加入和退出,同时还要支持多种被测产品的测试,因此,协同中的这些高阶指令不能简单地处理为一阶数据交互,需要给出这些设备指令的高阶封装规范和交互协同机制.

在安全苛刻系统测试过程中,协同涉及测试任务、测试设备以及被测产品三端之间的协同,这些协同行为既有时间上的协同,又有控制上的协同.为清晰协同关系,支持高阶协同系统上的相关性质分析,本文采用层次架构,将自动化测试系统分为测试任务端、测试设备端、被测产品端三端,通过对这三端和端之间交互定义,刻画测试过程中不同的协同关系.采用这种层次化架构,系统很容易扩展到对多被测产品的批产化网络测试.自动化模型层次架构如图 2所示.其中:测试任务端(TWPart)实现测试任务的组织和设计,实现对被测产品的自动化测试;测试设备端(TEQPTPart)支持上层测试任务对测试设备的访问和交互,为上层测试任务提供透明访问测试设备功能和屏蔽不同类设备的异构性,给出到具体测试设备的访问路由.被测产品端(PRODPart)完成测试设备到被测产品的交互,根据测试设备发来的激励、指令和请求,完成对被测产品状态参数的改变和获取.各端形式化定义如下:

定义1(测试任务端). 测试任务端TWPart=(TxTWEnvxTimer).其中,域T表示测试任务端测试任务,域TWEnv表示测试任务端测试任务的执行环境,域Timer为实时环境时钟域.

定义2(测试设备端). 测试设备端TEQPTPart=(TEQPTxHChannelxTInstructSet).其中,域TEQPT为测试设备,域HChannel为与测试任务端的交互通道,TEInstructSet为测试设备指令集域.

定义3(被测产品端). 被测产品端PRODPart=(PRODxPChannelxPInstructSet).其中,域PROD表示被测产品,域PChannel是与被测产品的交互通道,域PInstructSet表示被测产品的指令集域.

交互通道用于定义交互信息的形式,分为指令通道和数据通道,分别用于指令交互和数据交互.高阶的指令信息和一阶的数据信息形式化定义如下,是交互协议的形式表示:

定义4(交互指令). 交互指令域GuardV=G{Gd,Params},其中,

· G{}为标志符,用于标识{}内的高阶指令;

· 域Gd=(DevKindxOp)是测试指令的形式表示,域DevKind表示测试设备;域Op为具体指令的形式表示,是测试设备操作DevOp或被测产品操作ProdOp;

· 域Params为操作参数域Param上的序列.

定义5(交互数据). 交互信息域DataV=PParamxPVal.由被测产品状态参数名域PParam和参数取值域PVal组成.

定义6(被测产品操作). 被测产品操作ProdOp=PValxProdC®ProdC为一个函数域,其中,域PVal^*为被测产品状态参数取值域PVal上的序列;函数域ProdC为被测产品的状态,ProdC=PParam®PVal,是关于被测产品状态参数名域到状态参数取值域的映射.

定义7(测试设备操作). 测试设备操作域DevOp为函数域,DevOp=DValxDevC®DevCx(PParamxPVal),其中,域DVal^*为测试设备操作参数取值域DVal上的序列;函数域DevC为测试设备的状态,DevC=DParam® DVal,为测试设备操作参数名域DParam到值域DVal的映射.

将被测产品参数取值定义为被测产品的状态,被测产品的操作改变的是被测产品的状态.这里将被测产品的操作定义为高阶函数形式,即给定操作的参数值和被测产品的当前状态,返回的是操作作用被测产品之后的新状态.通过对被测产品操作的功能抽象来表示被测产品操作.由于测试设备操作改变的不仅是测试设备自身状态,还将产生关于被测产品的激励信号,以触发被测产品改变自身状态,激励信号可定义为对被测产品状态中某些相关参数改变取值,定义为(PParamxPVal)^*.

对给定的硬件设备,也就限定了该硬件设备上的所有操作,即设备和其操作集合之间存在着映射关系.下面给出了设备操作集域定义,表示测试设备、被测产品分别与其操作集合之间的映射关系.

定义8(设备类操作集). 设备类操作集域OpEnv为函数域,OpEnv=OpKind®OpS,是设备类OpKind到设备操作集合OpS的映射.函数域OpS为设备操作名标识OpId到域Op的映射,即,OpS=OpId®DevOp.

这样,在实际应用中,对给定的具体测试设备或被测产品,均可根据上述定义,给出该应用中被测产品和具体测试设备操作的高阶形式化定义.

若定义SCSAutTM为安全苛刻系统的自动化测试系统,根据上述定义,SCSAutTM为高阶协同系统:

SCSAutTM({TWPart,TEQPTPart,PRODPart},GuardV+DataV,Result):

TWPartxTEQPTPartxPRODPartResult.

3 安全苛刻系统自动化测试中的实时性

在安全苛刻系统自动化测试中,由于测试语言中基本元素为测试原子,测试原子的执行受时间约束,用以表明其内部测试行为执行的有效性.同时,测试原子上的复合操作也间接受时间影响.在一般语言系统中,系统行为改变系统状态,行为本身并没有结果,或者是结果无意义,主要用于系统调试.但安全苛刻系统自动化测试系统中,系统行为不仅改变系统自身状态,同时其本身的结果值也用于反映在时间约束下行为的有效性,即系统改变的状态是否正确.因此在测试模型中,测试原子及其上的复合操作均具有实时性.

若定义测试原子为Atom=Precond®AName(Time-Restriction)[TestP],其中,Time-Restriction即为测试原子的执行时间约束.测试原子上的复合操作如串行、并行、选择和循环等也受时间约束影响,称为时间约束串行、时间约束并行、时间约束选择和时间约束循环.对于测试原子,这些时间约束复合操作的含义分别:

· 时间约束串行“;_t”:测试原子之间时间约束串行指的是,只有当前一个测试原子的执行满足时间约束,且结果为真时,后续的测试原子才会被继续执行;否则中止,直接返回结果为假;

· 时间约束并行“||_t”:当且仅当两个测试原子的执行满足时间约束且结果均为真时,并行运行的结果才为真;否则为假;

· 时间约束选择if_t:当条件布尔表达式为真,其运行结果为第1个测试原子执行结果;否则为第2个的执行结果;

· 时间约束循环“while_t”:执行不仅依赖循环中的布尔表达式结果,而且还与循环体中的测试原子有关,当进入循环后,只有当循环体中的测试原子执行满足时间约束且结果为真时,才会返回到循环入口,继续循环;否则,结束循环.

从另一角度看,当测试过程中出现错误时,测试程序会终止后续动作的执行,并防止错误的测试操作对被测产品和测试设备的损坏,从而也保证了被测产品测试的安全性.

为刻画上述测试原子及其上复合操作的语义,定义时间约束函数监测测试原子的执行过程.若测试原子的执行过程可用函数描述,则时间约束函数一高阶函数形式.设测试原子的执行过程函数M^atom:AtomxContextx Timer®ResultxContext,Timer为时钟,Context为测试原子的上下文执行环境.时间约束函数TR定义为:M^atomx StartTimexTime-RestrictionxTimer®Result,Time-Restriction为测试原子的时间约束,StartTime为测试原子开始执行时间.对fÎM^atom,stÎStarttime,trÎTime-Restriction,tÎTimer,TR(f,st,tr,t)具体定义为:

(1) 若在t时钟下存在时刻t,st≤t<st+tr,f收敛.即f_t=…=f_st+tr=r,则TR(f,st,tr,t)=r;

(2) 否则,TR(f,st,tr,t)=false.

这样,通过TR函数时间约束测试原子的执行过程.

4 安全苛刻系统自动化测试模型SCSAutTM^** 4.1 被测产品PRODPart定义

被测产品端的主要功能是完成与测试设备端的交互协同.测试任务借助测试设备对被测产品进行测试,可以通过测试设备操作间接改变被测产品的状态信息.如卫星测试中,电源设备的加电操作产生对卫星的激励,使卫星通电.

定义9(被测产品). 自动化测试模型中,被测产品端PRODPart域中的被测产品PROD域定义为PROD= (ACKxProcCxProdOpS),其中,ACK为被测产品的响应动作,其他定义同上.

被测产品与测试设备的交互将通过PChannel完成.被测产品端的行为通过改变PChannel和自身状态参数实现与测试设备端的交互协同.被测产品端交互通道PChannel=PSendGSxPRetnVS.其中,指令通道PSendGS= (ANamexGuardV),数据通道PRetnVS=(ANamexDataVxLabel),AName为测试任务端的测试原子名,标志位Label用于标识一个交互动作是否已经完成.

被测产品端与测试设备端的交互过程为:

(1) 若接到关于自身的操作指令请求,则向测试设备端发送回令并执行具体操作;

(2) 若是来自测试设备的激励信号,则根据激励信号更新相应参数值,改变被测产品状态参数.由于激励是测试设备操作产生的,其回令已经由测试设备端收到测试设备操作时返回,故此时被测产品无需再返回回令;

(3) 若是被测产品状态参数请求,则将参数值传送给测试设备端.

被测产品端上的形式语义可表示为域PRODPart上语义映射函数M^Prodp,根据被测产品交互过程描述,其具体定义如图 3所示.

4.2 测试设备端TEQPTPart定义

测试设备端的主要功能是通过与测试任务端、被测产品端的交互支持测试任务完成对被测产品的测试.测试设备端将分别通过测试设备层的交互通道HChannel和被测产品层PChannel实现与测试任务端、被测产品的交互.同时,测试设备端还要完成交互中关于指令操作的静态解析功能,即检查交互信息是否符合协议,支持测试任务端和具体测试设备的交互.

测试设备端的测试设备由对被测产品测试中使用的各种测试仪器、测试系统等测试设备资源组成.测试设备的类型、数目众多,测试语言要独立于具体测试设备,需要与这些具体测试设备解耦合.为此,在测试语言中对测试设备进行分层:上层称为测试设备通信中间件(MTP),面向应用,旨在屏蔽前端测试应用功能级的复杂性,为测试任务提供透明的测试设备访问功能,其功能相当于应用级测试设备网关;其下层称为设备应用层(DAPP),屏蔽不同类设备的异构性,其功能相当于设备级测试设备网关;最底层为测试设备类层DK,DK管理具体的一类测试设备,给出具体测试设备的访问路由.通过这种分层架构,屏蔽底层测试设备的异构性,建立测试设备抽象描述、协同交互与统一访问机制.测试设备端架构如图 2所示.

定义10(测试设备). 自动化测试模型中,测试设备端TEQPTPart域中的测试设备TEQPT域定义为TEQPT= (MTPxDAPPxDKxBChannelxDChannel),其中,MTP(middleware of test process)称为应用级测试设备网关,域DAPP(device application)称为设备级测试设备网关,通道BChannel=BSendGSxBRetnVS为MTP与DAPP两层之间的交互通道,分为指令通道BSendGS=(ANamexGuardVxRtn)和数据通道BRetnVS=(ANamexDataVxLabel)表示来自测试原子的数据信息和指令信息.通道DChannel=DSendGSxDRetnVS为DAPP与DK两层之间的交互通道,分为指令通道DSendGS=(ANamexGuardVxRtn)和数据通道DRetnVS=(ANamexDataVxLabel)表示来自测试原子的数据信息和指令信息.其他定义同上.

测试设备层与测试任务层的交互通道HChannel=ASendGSxARetnVS,分为指令通道域ASendGS=(ANamex GuardVxRtnxLabel)和数据通道域ARetnVS=(ANamex DataVxLabel).返回值域Rtn=Bool+(BoolxString),其值或者为true,表示指令成功;或者为(false,errocode),表示指令执行失败,返回false和失败原因errocode;标志位Label含义同上.

测试设备端的形式化语义表示为TEQPTPart域上的映射函数M^Tep,定义为

M^Tep:TEQPTPartxPChannelxPInstructSet®HChannelxPChannel.

即,M^Tep:TEQPTxHChannelxTInstructSetxPChannelxPInstructSet®HChannelxPChannel.

这样,对于MtpÎMTP,DappÎDAPP,DkÎDK,zÎBChannel,hÎHChannel,VÎDChannel,r^TÎTInstructSet,xÎ PChannel,r^PÎPInstructSet,测试设备端的语义函数M^Tep具体定义为

M^Tep【(Mtp,Dapp,Dk,z,V)】(h,r^T,x,r^P)=M^Mtp【Mtp】(h,z)|M^Dapp【Dapp】(z,V,r^T,r^P)|M^Dk【Dk】(V,x).

其中,函数M^Mtp为应用级测试设备网关语义函数,M^Dapp为设备级测试设备网关语义函数,“|”表示并行.

若M^Mtp【Mtp】(h,z)=(h¢,z¢),M^Dapp【Dapp】(z,V,r^T,r^P)=(z¢,V¢),M^Dk【Dk】(V,x)=(V¢,x¢)

则M^Tep【(Mtp,Dapp,Dk,z,V)】(h,r^T,x,r^P)=(h¢,x¢).

M^Mtp,M^Dapp和M^Dk的具体定义见第4.2.1节~第4.2.3节.

4.2.1 应用级测试设备网关MTP

MTP端是由若干MTP进程以并行方式组成.MTP端进程的主要功能是对HChannel中的指令和参数请求传递给测试设备的通道BChannel中,并将测试设备的返回结果通过BChannel回传给HChannel.由于MTP端的时间约束是由测试任务端的测试原子来完成,即MTP端的实时性由测试任务端的实时性刻画,故此处MTP进程并行的执行同传统程序设计语言中的并行语义.若定义Mtp为MTP端进程,由于MTP端进程的功能是响应来自测试任务端的指令或参数请求,故进程Mtp和Mtps语法定义为:

Mtps::=Nil|Mtp||Mtps

Mtp::=MName[MtP]

MtP::=Nil|AName?GuardV|AName!DataV

其中,Nil表示空动作;a?gv和a!dv分别表示从测试任务端的测试原子a处获取指令gv和向测试原子a发送参数dv动作.

当MTP接收到来自测试任务层的数据请求时,通过对请求解析,将该请求发到指定的DAPP中并获取返回值返回到测试任务层;当接收到来自测试任务层的指令请求时,也同样解析该指令,判断发送给哪类DAPP,将该指令发送给该类DAPP,并将获取的回令返回给测试任务层.若定义M^M函数为MTP端进程的语义函数,M^M的定义如图 4所示.其中,函数Analy为MTP端的解析函数,根据给定的测试设备类DevKind和测试设备类与设备级测试设备网关映射表DD,找到该设备类所从属的设备级测试设备网关.DD=DevKind®DAPPName,其中, DAPPName为设备级测试设备网关名域,Analy:DevKindxDD®DAPPName.

4.2.2 设备级测试设备网关DAPP

设备级测试设备网关主要是检查和响应来自MTP端的指令操作或参数请求,即对MTP发来的请求进行解析,判断该请求是发送给哪类测试设备,并对其中交互信息进行协议检查,判断是否符合协议定义.定义函数Check:GNamexParamsxInstructSet®BOOL为协议检查函数,在指令集InstructSet检查指令GName及其参数Params是否符合定义.

当接收到数据请求时,将该请求通过指定类型的测试设备发送给被测产品;若接收到指令请求时,检查是否符合协议,符合则将该指令转发给指定设备(类),否则返回协议检查错误编码,回令置为false.若设备级测试设备网关层DAPP的语义函数M^Dapp,DAck为DAPP层响应动作,具体定义如图 5所示.

4.2.3 测试设备层TE

测试设备层TE根据具体设备的状态信息,找到合适设备执行数据请求或指令请求.完成到具体测试设备的访问.

当接收到关于被测产品状态参数值的数据请求时,则找到合适的设备将该请求发给该被测产品并获取参数值;当接收到关于自身的操作指令时,则找到合适的设备执行该指令,并将执行该指令产生的激励信号发送给被测产品;当接收到关于被测产品的指令请求时,则通过具体设备将该指令发给被测产品,并将被测产品发来的回令返回给上层.设备层的进程Dev可定义为:

Dev::=DevKind[OpId,Vals]|DevKind(OpId,Vals)|DevKind(PParam),

其中,d[f,as]表示接受到关于测试设备的指令,d是设备类名,f是d上的操作,as为参数值;d(g,ps)表示接受到,通过测试设备d传送的关于被测产品的指令g,ps为参数值;d(pn)表示通过测试设备d请求被测产品状态参数pn的值.根据上述测试设备层的功能描述,其语义定义如图 6所示.其中,DevInfo为测试设备信息环境,用于标识测试设备的使用状态,DevInfo=DevId®{‘Busy’,‘Idle’},DevId为测试设备名域.函数lookupId:DevKindxDevInfo® DevId,lookupId(dk,e)为在当前测试设备信息环境e下,在设备类dk中寻找适合的具体测试设备名.

测试原子进程为测试任务端基本测试进程,具体见本文第4.3节测试任务端定义部分.

4.3 测试任务端TWPart定义 4.3.1 TWPart语法

在测试任务层,通过对基本测试方法与操作的规范与封装,定义测试过程中的基本测试动作——测试原子.测试原子通过其内部动作与测试设备、被测产品进行指令与数据交互,并根据接收到的测试数据信息进行判别,完成一个相对独立的测试过程.之后,按照被测产品功能部件之间的逻辑关系,定义测试原子上的控制结构组成测试原子序列.这样,关于被测产品的测试任务由组成测试任务的测试原子序列来描述.

一般情况下,测试原子具有前置条件,当前置条件满足时,测试原子才能执行.同时,由于实时性的影响,每个测试原子具有时间约束,表示测试动作在一定时间范围内的有效性.因此,在测试系统中,测试原子可抽象定义如下:

定义11(测试原子). 自动化测试模型中,测试原子域Atom定义为Atom=Precond®AName(Runtime)[TestP],其中,Precond为布尔表达式,表示测试原子的前置条件;AName为测试原子名;Runtime为测试原子时间约束.联合域TestP为组成测试原子的内部动作,是由与测试设备端发生的交互动作ComA、判别动作Judge和关于时间的等待动作Wait组成.即,TestP=ComA+Judge(NumxTypexVal)+Wait(Num).联合域ComA包括向测试设备端的MTP发送指令MName!GuardV和从MTP接收参数MName?DataV两种动作,即,ComA=MName?DataV+ MName!GuardV.其中,“+”表示域的联合.

因此,测试任务端的测试任务T语法定义为

T::=skip|AtomL||_tT|AtomL;_tT

AtomL::=skip|Atom;_tAtom L|Atom||_tAtomL

|while_t BExp do AtomL od

|if BExp AtomL else AtomL

其中,skip表示空,AtomL为由测试原子复合组成的测试原子序列.

4.3.2 TWPart的语义

测试任务端根据被测产品的测试需求形成测试用例,通过与测试设备端、被测产品端的交互,返回测试结果,完成对被测产品的测试.因此,测试任务端的形式语义可表示TWPart上映射函数M^Twp,定义为

M^Twp:TWPartxTEQPTPartxPRODPart®Result.

即M^Twp:(TxTWEnvxTimer)xTEQPTPartxPRODPart®Result.

测试任务端的测试行为由测试任务T完成,若定义测试任务T的语义函数为M^T,则M^T=M^Twp.而测试任务T由测试原子序列构成,故首先给出测试原子的语义函数,接着,通过给出测试原子序列的语义函数定义M^T.

测试任务端测试原子的功能是通过其内部动作与测试设备和被测产品的交互完成测试原子的测试过程.因此在自动化测试模型中,定义M^Atom为测试原子的语义函数,其定义为M^Atom:AtomxTWEnvxTimerx TEQPTPartxPRODPart®Result.其中,TWEnv为测试原子执行的外部环境,其他定义如上.若iÎTWEnv,tÎTimer, (Teqpt,h,r^T)ÎTEQPTPart,(Prod,x,r^P)ÎPRODPart,则对一个测试原子pc®a(rt)[tp],有:

M^Atom【pc®a(rt)[tp]】(i,t,(Teqpt,h,r^T),(Prod,x,r^P))=

M【pc】it®TR((M^AtTs【(a,tp)】(t,h)|M^Tep【Teqpt】(h,x,r^T,r^P)|M^Prodp【Prod】x),t(time),rt,t),false.

其中,M^AtTs函数为测试原子a内部动作tp的执行语义函数,下面将具体讨论.

若M^AtTs【(a,tp)】(t,h)=(r,h¢),M^Tep【Teqpt】(h,x,r^T,r^P)=(h¢,x¢),M^Prodp【Prod】x=(g,x¢),则

M^AtTs【(a,tp)】(t,h)|M^Tep【Teqpt】(h,x,r^T,r^P)|M^Prodp【Prod】x=r.

测试原子通过其内部动作改变与测试设备端的通道HChannel内容来实现与测试设备端的交互,将测试原子的指令或参数请求发送给HChannel,并根据HChannel的返回结果给出测试原子的执行结果.测试原子内部动作的执行语义函数M^AtTs定义为ANamexTestPxHChannelxTimer®ResultxHChannel.即不考虑时间约束条件下,测试原子内部动作的执行过程描述.对一个测试原子a,hÎHChannel,tÎTimer,其内部动作执行的语义为:

· M^AtTs:ANamexTestPxHChannelxTimer®ResultxHchannel;

· M^AtTs【(a,nil)】h,t=(true,h);

· M^AtTs【(a,Judge(n,v))】h,t=n=?v;

· M^AtTs【(a,Wait(n))】h,t=k(n,t(time),t),其中,

k(n,ct,t)=t(time)-ct<n®k(n,ct,t),(true,h);

· M^AtTs【(a,m?(dk,dps))】h,t=W(m,a,h¢,t),其中,h¢¹(m,a)=(dk,dps,0),

;

· M^AtTs【(a,m!G{dk,dpop,ps})】h,t=¡(m,a,h¢,t),其中,h¢²(m,a)=(dk,dpop,ps,0),

.

对于判参操作Judge(n,v),判断状态参数n是否符合v.v可以表征某一范围值或者某一具体值.根据文献^[35],其判断都可以归为等式逻辑的判断操作,故用n=?v形式表示状态参数n是否符合v.

根据测试原子的语义函数和测试原子上的复合操作含义,容易给出测试原子序列的语义函数M^AtomL,主要包括测试原子上时序串行、并行、循环和选择等复合操作的语义:

· M^AtomL:AtomLxTWEnvxTimerxTEQPTPartxPRODPart®Result;

· M^AtomL【skip】(i,t,Tep,Prodp)=true;

· M^AtomL【atom;_tatomL】(i,t,Tep,Prodp)=M^Atom【atom】(i,t,Tep,Prodp)®M^AtomL【atomL】(i,t,Tep,Prodp), false;

· M^AtomL【atomL₁||_tatomL₂】(i,t,Tep,Prodp)=r₁Ùr₂,其中,

r₁=M^AtomL【atomL₁】(i,t,Tep,Prodp),r₂=M^AtomL【atomL₂】(i,t,Tep,Prodp);

· M^AtomL【while_t b do atomL od】(i,t,Tep,Prodp)=¶(i,t,Tep,Prodp),其中,

¶(i,t,Tep,Prodp)=M【b】(i,t)®(r®y(i,t,Tep,Prodp),true),true,

其中,r=M^AtomL【atomL】(i,t,Tep,Prodp);

· M^AtomL【if_t b atomL₁else atomL₂】(i,t,Tep,Prodp)=M【b】(i,t)®M^AtomL【atomL₁】(i,t,Tep,Prodp),

M^AtomL【atomL₂】(i,t,Tep,Prodp).                                         

这样,测试任务T上的语义函数M^t定义为:

· M^t:TxTWEnvxTimerxTEQPTPartxPRODPart®Result;

· M^t【skip】(i,t,Tep,Prodp)=true;

· M^t【atoml;_tt】(i,t,Tep,Prodp)=r®M^t【t】(i,t,Tep,Prodp),false,其中,r=M^AtomL【atoml】(i,t,Tep,Prodp);

· M^t【atoml||_tt】(i,t,Tep,Prodp)=r₁Ùr₂,其中,r₁=M^AtomL【atoml】(i,t,Tep,Prodp),r₂=M^t【t】(i,t,Tep,Prodp).

5 安全苛刻系统自动化测试模型SCSAutTM相关性质

由于涉及高阶协同和4类时间约束复合操作,需阐述模型的正确性和收敛性.以下将给出模型的收敛性和正确性证明.

5.1SCSAutTM的收敛性

定理1. 在自动化测试模型中,对任意测试原子,其上的语义函数M^Atom是收敛的.

证明:在自动化测试模型中,对一个测试原子pc®a(rt)[tp],有:

M^Atom【pc®a(rt)[tp]】(i,t,(Teqpt,h,r^T),(Prod,x,r^P))=

M【pc】it®TR((M^AtTs【(a,tp)】(t,h)|M^Tep【Teqpt】(h,x,r^T,r^P)|M^Prodp【Prod】x),t(time),rt,t),false.

设:

· G=M^Atom【pc®a(rt)[tp]】(i,t,(Teqpt,h,r^T),(Prod,x,r^P));

· H=M^AtTs【(a,tp)】(t,h)|M^Tep【Teqpt】(h,x,r^T,r^P)|M^Prodp【Prod】x);

· F=TR(H,t(time),rt,t),

则G=M【pc】it®F,false.

当前置条件不满足时,测试原子不执行,返回结果为false,收敛.以下证明当前置条件为真时,测试原子的执行过程收敛.采用结构归纳法证明:

(1) 当tp=Skip时,M^AtTs【(a,nil)】(t,h)=(true,h),H=true,F=TR(true,t(time),rt,t)=true,收敛.

(2) 当tp=Wait时,M^AtTs【(a,Wait(n))】h,t=k(n,t(time),r,t),其中,递归函数k(n,ct,t)=t(time)-ct<n®k(n,ct,t), (true,h).由于时钟t为增函数,存在某时刻tÎTIME,使t-ct>n,即函数k最终将收敛为(true,h),H=true,F=TR(true, t(time),rt,t)=true.若$t¢ÎTIME,设st=t(time),t-ct<n且t-st>rt,则根据TR定义,F=false.故收敛.

(3) 当tp=Judge时,M^AtTs【(a,Judge(n,v))】h,t=((n=?v),h),H=(n=?v),F=TR((n=?v),t(time),rt,t).F的结果即为(n=?v).故收敛.

(4) 当tp=m?(dk,dps)时,M^AtTs【(a,m?(dk,dps))】h,t=W(m,a,h¢,t),其中,h¢¹(m,a)=(dk,dps,0),函数W的含义见上.令st=t(time),F=TR(H,st,rt,t),若$t,t-st>rt,H函数未收敛,则据TR定义,F=false;若$t,t-st<rt,H函数收敛,则收敛.以下证明:在理想情况下,函数H=W(m,a,h¢,t)|M^Tep【Teqpt】(h¢,x,r^T,r^P)|M^Prodp【Prod】x收敛:

根据上述定义,对Teqpt=(Mtp,Dapp,Dk),有:

M^Tep【Teqpt】(h¢,x,r^T,r^P)=M^Tep【(Mtp,Dapp,Dk)】(r^T,h¢,x,r^P)

                                                =M^Mtp【Mtp】(h¢,z)|M^Dapp【Dapp】(z,x,r^T,r^P)|M^Dk【Dk】(V,x).

对M^Mtp【Mtp】(h¢,z):

· 若当Mtp¹m[a!(dk,dps)]时,即没有响应测试原子a的请求时,F函数不终止,W(m,a,h¢,t)函数也将不终止.根据TR定义(步骤(2)),则H=false终止;

· 当Mtp=m[a!(dk,dps)]时:

* M^Mtp【Mtp】(h¢,z)=F(h¢,z¢);

* M^Tep【Teqpt】(h¢,x,r^T,r^T)=F(h¢,z¢)|M^Dapp【Dapp】(z¢,V,r^T,r^P)|M^Dk【Dk】(V,x).

其中,z¢¹(m,dapp)=Add BRetnVS(a,dk,dps,0).

在DAPP层,根据给定定义,有M^Dapp【dack】(z¢,V,r^T,r^P)=f(z¢,V¢),其中,V¢¹(dapp,dk)=Add DRetnVS(a,dk, dps,0),f定义见上.此时有M^Tep【Teqpt】(h¢,x,r^T,r^T)=F(h¢,z¢)|f(z¢,V¢)|M^Dk【Dk】(V,x).

在TE层,对eÎDevInfo,dÎDevC,cÎOpEnv,根据给定定义有M^Dev【(dk(dps),e,d,c)】(V¢,x)=q(V¢,x¢),其中,x¢¹(dk) =Add DRetnVS(a,dk,dps,0),q定义见上.此时,M^Tep【Teqpt】(h¢,x,r^T,r^T)=F(h¢,z¢)|f(z¢,V¢)|q(V¢,x¢).

在PROD端,设(ack,g,¡)ÎPROD,(pn,pv)=dps,M^Prodp【(ack,g,¡)】x¢=(g,x²),其中,

pv=g(pn),x²¹(dk)=Update PRetnVS(a,dk,(pn,pv),1).

因此,

H=W(m,a,h¢,t)|F(h¢,z¢)|f(z¢,V¢)|q(V¢,x¢)|(g,x²)

=W(m,a,h¢,t)|F(h¢,z¢)|f(z¢,V¢)|(V²,x¢²)|(g,x¢²),V²¹(dapp,dk)=Update DRetnVS(a,dk,(pn,pv),1),

                                                                        x¢²(dk)=Del PRetnVS(a,dk,(pn,pv),1)

=W(m,a,h¢,t)|F(h¢,z¢)|(z²,V¢²)|(V¢²,x¢²)|(g,x¢²),z²¹(m,dapp)=Update BRetnVS(a,dk,(pn,pv),1),

                                                                        V¢²¹(dapp,dk)=Del DRetnVS(a,dk,(pn,pv),1)

=W(m,a,h¢,t)|(h²,z¢²)|(z¢²,V¢²)|(V¢²,x¢²)|(g,x¢²),h²¹(m,a)=Update ARetnVS(dk,(pn,pv),1),

                                                                        z¢²¹(m,dapp)=Del BRetnVS(a,dk,(pn,pv),1)

=W(m,a,h¢²,t)|(h¢²,z¢²)|(z¢²,V¢²)|(V¢²,x¢²)|(g,x¢²),h¢²¹(m,a)=Del ARetnVS(a,dk,(pn,pv),1)

=true故收敛.

但上述计算过程的递归函数不中止时,根据TR定义(步骤(2)),则H=false终止.

(5) 当tp=m!gv时,其过程同步骤(4),可证明同样函数H收敛.

定理2. 在自动化测试模型中,由测试原子通过时间约束串行、时间约束并行、时间约束循环和时间约束选择复合操作组成的测试任务T,其语义函数M^T是收敛的.

证明:由定理1,根据测试原子上时间约束串行、时间约束并行、时间约束循环和时间约束选择复合操作语义函数定义,容易证明.篇幅有限,此处略去.

5.2SCSAutTM的正确性 5.2.1 安全苛刻系统自动化测试过程的抽象描述

本节将给出安全苛刻系统自动化测试的抽象机,用于描述安全苛刻系统自动化测试的实际测试过程.由于安全苛刻系统自动化测试具有实时性,定义表示转换的前提,测试任务与测试设备交互返回值a为系统转换标记,即“®_a”,“®”表示无交互返回值;“”表示“®_a”È“®”.下述用stÎTIME,tÎTimer表示在实时环境t和某一时刻st下的转换前提.Timenotout:TimerxTimexTime-restriction®Bool函数用于监测计算过程是否超时:若超时,则为真;否则为假.实际测试过程的抽象语义描述为:

(1) 空规则:当测试原子a中的测试动作为空操作skip时,直接返回true结果.即:

stÎTIME,tÎTimera(rt)[Nil]®true.

(2) Wait规则:当测试原子a中的测试动作为等待操作Wait(n)时,若在等待操作执行过程中a超时,则终止等待动作;否则,等待指定的n个时间段.即:

_{stÎTIME,tÎTimer};

_{stÎTIME,tÎTimer}.

(3) Judge规则:当测试原子a中的动作为判参操作Judge(n,v)时,根据参数的名字和值v判断是否符合参数定义.若在执行过程中a超时,则终止判参操作,返回false结果;否则,返回判参结果.即:

_{stÎTIME,tÎTimer};

_{stÎTIME,tÎTimer}.

(4) 交互指令规则:当测试原子a中的动作为发指令操作m!gv时,a将通过测试设备端的MTP将指令gv传给测试设备或被测产品,返回回令true.同样地,若在执行过程中a执行超时,则终止该动作的执行,返回false结果.即:

_{stÎTIME,tÎTimer};

_{stÎTIME,tÎTimer}.

(5) 交互参数规则:当测试原子a中的动作为取参数操作m!dv时,a将通过测试设备端的MTP向被测产品发出请求,取回参数值,返回true.同样地,若在执行过程中a执行超时,则终止该动作的执行,返回false结果.即:

_{stÎTIME,tÎTimer};

_{stÎTIME,tÎTimer}.

(6) 复合规则:对a,a₁,a₂ÎAtomL:

① 时间约束串行规则(;_t-rule):a₁;_ta₂=a₁®a₂,false;

② 时间约束并行规则(||_t-rule):a₁||_ta₂=a₁Ùa₂;

③ 时间约束循环规则(while_t-rule):while_t b do a od=j,其中,j=b®(a®j,false),false;

④ 时间约束选择规则(if_t-rule):if_t b then a₁ else a₂=b®a₁,a₂.

5.2.2 SCSAutTM的正确性证明

定理3. 在自动化测试模型中,对任意测试原子,其执行语义函数M^Atom的执行结果与测试原子的抽象语义一致.

证明:在自动化测试模型中,对一个测试原子pc®a(rt)[tp],有:

M^Atom【pc®a(rt)[tp]】(i,t,(Teqpt,h,r^T),(Prod,x,r^P))=

M【pc】it®TR((M^AtTs【(a,tp)】(t,h)|M^Tep【Teqpt】(h,x,r^T,r^P)|M^Prodp【Prod】x),t(time),rt,t),false.

设:

· G=M^Atom【pc®a(rt)[tp]】(i,t,(Teqpt,h,r^T),(Prod,x,r^P));

· F=TR((M^AtTs【(a,tp)】(t,h)|M^Tep【Teqpt】(h,x,r^T,r^P)|M^Prodp【Prod】x),t(time),rt,t),

则G=M【pc】it®F,false.

当前置条件不满足时,测试原子不执行,返回结果为false.以下证明当前置条件为真时,测试原子的执行与测试过程中测试原子的抽象语义一致.采用结构归纳法证明:

(1) 当tp=Skip时,M^AtTs【(a,nil)】(t,h)=(true,h),F=TR(true,t(time),rt,t)=true,符合测试原子的空规则.

(2) 当tp=Wait时,M^AtTs【(a,Wait(n))】h,t=k(n,t(time),r,t),其中,递归函数k(n,ct,t)=t(time)-ct<n®k(n,ct,t), (true,h).由于时钟t为增函数,存在某时刻tÎTIME,使t-ct>n.即,函数k最终将收敛为(true,h),F=TR(true,t(time),rt, t)=true.若$t¢ÎTIME,设st=t(time),t-ct<n且t-st>rt,则根据TR定义,F=false.符合Wait规则.

(3) 当tp=Judge时,M^AtTs【(a,Judge(n,v))】h,t=(n=?v),F=TR((n=?v),t(time),rt,t).F的结果即为(n=?v).符合Judge规则.

(4) 当tp= m?dv时,见第5.1节.符合交互参数规则.

(5) 当tp=m!gv时,见第5.1节.符合交互指令规则.

定理4. 在自动化测试模型中,由测试原子通过时间约束串行、时间约束并行、时间约束循环和时间约束选择复合操作组成的测试任务,其语义函数M^T与测试任务的抽象语义一致.

证明:由定理3,根据测试原子上时间约束串行、时间约束并行、时间约束循环和时间约束选择复合操作语义函数定义,容易证明.篇幅有限,此处略.

6 结论及未来工作

基于安全苛刻系统的可信性需求,在已有工作的基础上,通过对安全苛刻系统自动化测试分析,采用指称语义形式化方法,为安全苛刻系统的自动化测试建立了一种层次化高阶实时时序演算模型.本文通过对测试过程中高阶协同性的分析和定义,以论域理论为基础,给出自动化测试模型.该模型是一种由测试任务端、测试设备端和被测产品端组成的层次化架构,通过对三端高阶域及其域上方程定义,给出三端的形式化语义,定义了自动化测试模型.通过这种层次化描述,刻画了自动化测试过程中测试动作之间的控制协同和时间协同关系.通过对被测产品、测试设备与测试任务的抽象与组织,给出安全苛刻系统测试的信息化工作模式,实现安全苛刻系统自动化测试系统的组织结构、测试流程等的标准化定义.最后,通过对模型中高阶域上方程的收敛性和正确性的证明论证了自动化测试模型高阶协同行为的可计算性,验证了安全苛刻系统测试的可自动化.该模型可直接推广到多被测产品的批产化网络测试中.由于篇幅所限,将另文讨论模型的实时性和时序性.

未来工作将继续给出模型的实时性和时序分析与讨论;研究基于此模型的测试语言的设计和实现,包括测试设备操作等高阶指令的封装规范以支持测试语言的通用性,测试语言的控制结构定义以及测试语言实现中的并行、实时、时序等关键问题,以支持语言的实时、时序性;研究安全苛刻系统测试的测试需求描述语言,由于测试需求描述具有时序性,测试需求中测试参数(即被测产品状态)具有时序性,研究测试需求中测试参数之间满足的时序规约关系,形成对测试需求的合理表示;同时,将研究带时序的测试需求可满足定义和验证推理系统,验证测试需求的可满足性等;研究测试过程中测试设备的协同问题,包括测试设备的冲突定义、冲突发生条件和冲突消解规则,使测试设备在测试过程中能够检测冲突和消解冲突等.