第39卷  计算机学报  Vol.39 2016 论文在线出版号  No.170  CHINESE JOURNAL OF COMPUTERS  Online Publishing No.170 ——————————————— 本课题得到国家自然科学基金(No.91218302,  No.61472197)；北京市自然科学基金(No.4132062)资助.王博，男，1979年生，博士研究生，主要研究领域为软件测试、嵌入式系统，E-mail:  w-b11@mails.tsinghua.edu.cn.白晓颖，女，1973年生，博士，副教授，计算机学会(CCF)会员（会员号:  E200006012M），主要研究领域为软件测试、服务计算，E-mail: baixy@tsinghua.edu.cn.陈文光，男，1972年生，博士，教授，计算机学会(CCF)会员（会员号:  E200006533D），主要研究领域为并行与分布式计算，E-mail: cwg@tsinghua.edu.cn.  Xiaoyu  SONG，男，1963年生，博士，教授，主要研究领域为形式化方法、嵌入式计算系统，E-mail: song@ece.pdx.edu.  王  博1),2)  白晓颖1),2)    陈文光1),2)    Xiaoyu SONG3) 1)(清华大学计算机科学与技术系    北京    100084) 2)(清华大学信息科学与技术国家实验室    北京    100084) 3)(波特兰州立大学电气与计算机工程系  波特兰  美国  97207)  摘  要  时序特性是嵌入式软件的重要特性，实时嵌入式软件运行的正确性不仅依赖于任务执行结果，更依赖于任务执行时间。执行任务往往具有多个时间约束，且相互之间可能存在制约关系，对时间约束进行验证和确认是嵌入式软件测试的一个重要问题。本文提出一种基于执行片段的嵌入式软件时序特性检测方法(Trace-Based Temporal Defect Detection, TBTDD)。一方面，基于扩展语义接口自动机(Extended  Semantic  Interface  Automata,  ESIA)模型，刻画嵌入式软件时序特性需求，分析不同时间约束间存在的相关关系类型，并提出基于相关矩阵的相关时间约束识别算法；另一方面，在目标软件运行环境中提取包含时间信息的执行片段，通过执行片段与时间约束模型的匹配，依据预先制定的时序特性检测准则，检验执行序列是否满足模型中各项独立、相关时间约束的要求，进而发现被测软件中存在的时序缺陷。实验以卫星定位系统软件为例进行建模与缺陷检测，并在执行片段集、缺陷检测能力等方面进行了对比分析。实验表明，该方法可有效检测软件运行过程中存在的各类异常时序，提高了软件时序测试的有效性和充分性。 关键词  接口自动机;  时间约束;  执行片段;  相关性分析;  时序缺陷检测 中图法分类号  TP311 论文引用格式 王 博，白晓颖，陈文光，Xiaoyu SONG，基于执行序列的嵌入式软件时序异常检测，2016，Vol.39：在线出版号 No.170 WANG Bo，BAI Xiao-Ying，CHEN Wen-guang，Xiaoyu SONG，Temporal Defect Detection of Embedded Software Using Timed Execution Trace， Chinese Journal of Computers,2016, Vol.39: Online Publishing No.170  Temporal Defect Detection of Embedded Software Using Timed Execution Trace WANG Bo 1),2)  BAI Xiao-Ying 1),2)  CHEN Wen-guang1),2)  Xiaoyu SONG 3) 1)(Department of Computer Science and Technology,    Tsinghua University,    Beijing    100084) 2)(National Laboratory for Information Science and Technology,    Tsinghua University,    Beijing    100084) 3)(Department of Electrical and Computer Engineering,    Portland State University,    Portland,    USA,    97207)  Abstract Temporal requirements are critical to embedded software. The correctness of system operation depends on its satisfication to the timing constraints. In an embedded system, there usually exist many timing constraints which may also correlate with each other. It is important to ensure that the execution of the system conforms to its temporal requirements. The paper proposes an approach for detecting temporal defects based on execution traces 网络出版时间：2016-11-18 21:31:06网络出版地址：http://www.cnki.net/kcms/detail/11.1826.TP.20161118.2131.002.html2  计算机学报  2016年 analysis. The  characteristics  of  timing  constraints  are  analyzed,  and  the  ESIA  (Extended  Semantic  Interface Automata) is proposed to characterize temporal requirements of embedded software. Then the correlation patterns of timing  constraints  are analyzed,  and  an algorithm using  timing matrix  is  proposed  to  identify  the  correlated timing constraints in ESIA model. Traces tagged with time stamps are gathered from the execution environment of the target software. According to the temporal checking rules predefined, the traces are matched to the temporal model  to  verify  its  conformance  to  timing  constraints,  both  individual  as  well  as  correlated  constraints.  In  case violations  detected,  potential  defects  will  be  reported  for  further  investigation.  Experiments  are  exercised  on  a satellite positioning system for modeling and defect detection. The results are compared with other approaches in terms traces analysis and defect detection capabilities. It showed that the proposed approach can effectively detect temporal  anomalies  in  system  execution, which enhance the  effectiveness  and efficiency of  temporal  testing  of embedded software. Key words  interface automata; timing constraint; execution trace; correlation analysis; temporal defect detection   1  引言 时序特性是否满足设计要求将对实时嵌入式软件运行产生关键影响，时序异常可能造成任务执行失败，甚至对系统造成破坏性影响。特别在具有高实时、高安全性要求的应用领域内，如航空机载任务系统、航天发射控制、高速铁路运控等，各项任务的执行具有严格时间约束，对系统的安全、高效运行起着至关重要的作用。因此，保证嵌入式软件时序设计、实现的正确性是嵌入式软件开发的重要任务。 嵌入式软件时序测试是检验嵌入式软件时序特性是否满足设计要求、保证软件质量的重要手段。传统时序测试方法需要介入甚至控制软件运行过程，其核心是测试用例设计。在特定运行场景下，通过在目标软件运行环境中设置激励、预置数据，控制其按预期方式运行，随后观察、采集运行结果，并检查运行结果是否满足设计要求。 随着嵌入式软件规模、复杂度的不断上升，传统时序测试方法面临一些困难和局限性，时序测试与验证愈发成为一项困难的工作。首先，在某些情况下，测试人员无法直接获得目标软件控制接口，无法暂停、终止、或介入软件运行过程，造成部分场景无法设置，部分用例无法执行；由于仪器性能限制、数据观测误差等，测试人员无法从外部采集精确的运行时间信息；当嵌入式软件是由多个构件组成的分布式系统时，测试人员难以协调控制各构件间的运行时序。以上因素均可能造成嵌入式软件时序特性测试不充分、结果不准确。 其次，嵌入式软件中往往存在大量时间约束，限制各项任务的执行时间。不同任务的执行路径可能相互重叠，其执行时间之间可能存在特定依赖关系，从而造成相应时间约束之间间接相关。因此，在时序测试中，不仅需检验各项任务的执行时间是否满足相应时间约束，还需检验任务的执行时间是否满足此类依赖关系，以检测可能的时序异常，而传统测试方法难以针对此类相关时间约束进行测试。 再次，由于对目标软件理解、以及测试环境条件的局限性，通常情况下，设计的测试用例集难以完全覆盖软件运行过程中的各类正常、异常时序，特别是难以对偶发的异常时序进行测试。 针对以上问题，本文提出一种基于执行序列的时序缺陷检测方法(Trace-Based Temporal Defect Detection,  TBTDD)。相对于传统时序测试方法，TBTDD无需控制目标软件运行，而通过持续监视过程，提取一组包含时间信息的执行片段，进而根据目标软件形式化描述，对收集的软件运行信息进行离线自动检测，以考察软件实现是否满足设计要求。TBTDD方法可识别执行路径上不同时间约束间的相关关系，并对不同任务执行时间之间的依赖关系进行检测。TBTDD方法可伴随目标系统交付运转过程执行，通过长期收集有效的执行片段，积累丰富的运行场景，实现对目标软件各类正常、异常时序的充分检测。本文主要内容如下： 1.  时序特性分析与建模。对嵌入式软件时序特性进行分析，在扩展语义接口自动机(Extended Semantic  Interface  Automata,  ESIA)模型中定义时间变量、置零行为、时间约束等元素，建立ESIA模型时序语义，支持嵌入式软件时序特性的定量、精确描述。 论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  3 2.  时间约束相关性分析。在ESIA模型的特定执行路径之上，分析不同时间变量的取值之间可能存在的依赖关系，据此定义不同时间约束间的包含相关、交叉相关关系。 3.  TBTDD方法及算法。对嵌入式软件运行时序检测流程进行分析与讨论，在ESIA模型之上定义包含时间信息的执行片段，制定执行片段可接受性准则，提出执行片段匹配、时序缺陷检测等算法，以检查嵌入式软件执行序列包含的时间信息是否满足设计要求。 实验结果显示，TBTDD方法可有效检测嵌入式软件执行片段中存在的各类时序缺陷，特别是违反相关时间约束、异常时序处理错误等缺陷，与传统时序测试方法配合使用时，可对目标软件时序特性进行更充分的测试。TBTDD方法不需要预先设计测试用例与测试场景，降低了测试环境和人为因素对测试工作的限制与影响。TBTDD方法不会干扰软件正常运行，可获得准确的运行时序信息与测试结果。 本文第2节描述研究背景；第3节介绍ESIA模型时序语义相关内容，讨论不同时间约束之间的相关关系；第4节介绍TBTDD方法的工作原理与系列算法等；第5节介绍实验设计，以卫星定位系统软件为例，进行时序特性建模与时序缺陷检测，以验证本文方法的有效性；第6节叙述与本文研究相关的工作；第7节总结全文内容。 2  研究背景 精确与完整的建模是理解目标系统时序特性、开展时序缺陷检测的基础。近年来涌现出一系列时序特性定量描述模型，如时间自动机(Timed Automata, TA)、时序描述逻辑(Temporal Description Logics,  TDL)、统一建模语言(Unified  Modeling Language,  UML)、时间Petri 网(Timed  Petri  Net, TPN)、以及马尔科夫链(Markov Chain)等[1-3]，均可精确刻画嵌入式软件时序特性。 接口自动机(Interface  Automat,  IA)是一种轻量级的构件接口模型[4]。IA 模型通过状态机上的接口行为描述构件间的通信与交互过程，刻画系统外部行为特性，隐藏构件内部结构，是可组合嵌入式软件系统建模的有效工具。 定义1.  接口自动机IA[4].  嵌入式软件IA 定义为P=(VP, Von P, AI P, AO P, AH P, ΔP)，其中： VP是自动机包含的状态集合； Von P 是自动机包含的初始状态集合，Von P Í VP，若Von P =f，则称P为空； AI P、AO P、AH P分别为输入、输出、内部行为集合，AI P∩AO P=AI P∩AH P=AO P∩AH P=f；AP = AI P∪AO P∪AH P表示全部行为的集合； ΔPÍVP´AP´VP是自动机包含的状态迁移集合。 ESIA模型通过对IA 进行变量、执行约束等扩展，支持反应式嵌入式软件行为特性的建模与分析[5]。在ESIA模型中，引入输入、输出行为参数、内部计算变量、参数约束条件、以及行为前置/后置条件等，对软件运行过程中的数据信息进行描述。 定义2.  扩展语义接口自动机ESIA[5].  嵌入式软件ESIA 定义为P=(VP, Von P, XP, AP, YP, E, ΔP)，其中： VP是自动机包含的状态集合； Von P 是自动机包含的初始状态集合，Von P Í VP，若Von P =f，则称P为空； XR P、XH P分别为行为参数、内部变量集合，XR P∩XH P=f；其中内部变量描述软件维护的中间计算变量与计算结果；XP = XR P∪XH P表示全部变量的集合； AI P、AO P、AH P分别为输入、输出、内部行为集合，AI P∩AO P=AI P∩AH P=AO P∩AH P=f；AP = AI P∪AO P∪AH P表示全部行为的集合； YP是行为执行约束集合；aÎAP是一项行为，"y(a)ÎYP 是行为a 的一组执行约束，表示为y(a)=(PreCon(a), PostCon(a))，其中，PreCon(a)、PostCon(a)分别为行为a的前置、后置条件； E是触发事件集合，"eÎE触发P中特定行为的执行； ΔPÍVP´AP´VP是自动机包含的状态迁移集合，"δÎΔP表示一个状态迁移过程，具体描述如下： ( ) ( )' , ( ), ( ), ( );e PreCon a eff a PostCon aa qq d= ¾¾¾¾¾¾¾¾¾® 其中，δ.e表示行为触发事件，δ.a表示引起状态迁移的行为，δ. eff(a)表示行为a产生的执行效果，δ. PreCon表示行为a的前置条件，δ. PostCon表示行为a的后置条件，δ.s= q表示源状态，δ.t= q’表示目标状态。 在ESIA模型基础上，设计了一种基于符号执行的测试用例生成算法，通过搜索有效的事件/数据序列，自动生成测试用例与测试场景[5]。 4  计算机学报  2016年 3  嵌入式系统时序特性分析 本节以一个门禁控制系统为例，对嵌入式软件时序特性进行分析。在此基础上，定义时间变量、时间约束等时序元素，建立ESIA模型时序语义，支持嵌入式软件时序特性的定量描述与理解，并进一步分析不同时间约束之间存在的典型相关关系。 3.1  示例 门禁控制软件是一项典型的嵌入式软件，在特定事件触发下，按一定时序打开或关闭门禁，其ESIA模型如图1所示。 门禁控制软件根据接收到的人员抵近(approach)或离开事件(leave)，按设计时序执行打开门禁(open)、关闭门禁(close)、向控制中心上报当前状态(report)等行为。其中： ·  状态0是门禁系统上电初始状态； ·  当控制软件完成初始化后，进入等待状态1； ·  当检测到人员抵近后，进入状态2，准备打开自动门； ·  当自动门打开后，进入门禁打开状态3； ·  当检测到人员离开后，进入状态4，随即关闭自动门，返回等待状态1； ·  在自动门打开时（状态3下），门禁控制软件向监控中心周期上报状态信息并进入报告状态5，直到检测到人员离开后，退出周期上报过程。 0r epor t!appr oachappr oach ?open1clos e2leave?clos e!leave3open!r epor t5r etur n;4initializ atio n; 图1 门禁控制软件ESIA模型.其中，“？”表示输入行为，“！”表示输出行为，“；”表示内部行为. 在门禁控制软件中设定了一系列时间约束，具体包括： DC-TR1.  门禁控制软件在系统上电后5s时完成初始化； DC-TR2. 当检测到人员抵近后，自动门应在时间区间[3s, 7s]内打开； DC-TR3. 当检测到人员离开后，自动门应在时间区间[3s, 5s]内关闭； DC-TR4. 当检测到人员抵近后，应在时间区间[3s, 30s]内检测到相关人员离开； DC-TR5. 在自动门打开后，自动门应在30s内关闭，即自动门持续打开时间不应超过30s； DC-TR6. 在自动门打开时（状态3），门禁控制软件每15s 向监控中心上报一次自动门打开状态。 3.2  时间约束分析与建模 在嵌入式软件中，时间约束限制特定任务的执行时间，如任务开始、结束、或持续时间等。当执行时间满足时间约束时，软件将表现出符合设计预期的时序特性。B.Dasarathy将时间约束分为最小值约束、最大值约束以及持续约束[6]。其中，最小值、最大值约束分别描述两个事件之间的最小、最大时间间隔，而持续约束描述一个事件从产生到结束的持续时间。在本文中，根据限制对象的不同，分别定义以下三类时间约束。 定义3.  时间点约束：限制事件产生的时间点. 设τ为一项时间变量，t 为一个时间点，一项时间点约束定义为：P_Cstr(τ) = t，即τ = t。 定义4.  持续时间约束：限制任务执行持续时间，或者任务开始前等待时间.  设τ 为一项时间变量，一项持续时间约束D_Cstr(τ)定义为以tl 为下边界，以tu为上边界的时间区间，具体分为以下四种形式： D_Cstr(τ) = [tl, tu]，即tl £ τ £ tu； D_Cstr(τ) = (tl, tu]，即tl < τ £ tu； D_Cstr(τ) = [tl, tu)，即tl £ τ < tu； D_Cstr(τ) = (tl, tu)，即tl < τ < tu。 定义5.  周期时间约束：限制任务重复执行的时间间隔.  设τ为一项时间变量，t 为执行周期，一项周期时间约束定义为：C_Cstr(τ)=t，即Mod(τ, t)=0。 在门禁控制软件中，DC-TR1为时间点约束，DC-TR2/DC-TR3等为持续时间约束，DC-TR6为周期时间约束。τ ⊢ Cstr(τ)表示时间变量τ的取值满足时间约束Cstr(τ)。此外，通过逻辑运算符连接不同类型时间约束，可得到各种复杂时间约束表达式。 对ESIA模型进行时间变量、置零行为、时间约束等扩展如下。 定义6. ESIA时序语义. P=(VP, Von P, XP, AP, YP, E, ΔP)为一个ESIA ，其时序语义描述了一个基于接口事件与时间约束的状态迁移系统： 论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  5 XT P是一个有限时间变量集合，XP = XR P∪XH P∪XT P表示全部变量的集合；其中，"τÎXT P为一项时间变量，在ESIA模型空间内可重复置零并启动计时，以描述对不同行为的时间约束； "δÎΔP表示一个状态迁移过程，具体描述如下： ( ) ( )' , ( ), (),  ( ), ( ), ();e PreCon a reset eff a PostCon a reseta qq d= ¾¾¾¾¾¾¾¾¾¾¾¾® 其中，行为a的前置条件PreCon(a)包含行为a被激活时需要满足的时间约束，而后置条件PostCon(a)包含行为a正常结束时需要满足的时间约束。PreCon(a)与PostCon(a)均可包含多项时间约束，不同时间约束之间以逻辑运算符相连接，构成PreCon(a)与PostCon(a)的一阶逻辑表达式。由此，在行为的前置、后置条件中整合各类时间约束，对其执行的时间条件进行统一描述。设XT为被测软件ESIA模型的时间变量集合；XT 1 为行为a激活时完成计时的时间变量集合，XT 1 ÍXT；XT 2 为行为a完成时完成计时的时间变量集合，XT 2 ÍXT；行为a的前置、后置条件分别表示为： PreCon(a)=Cstr(τpre-1)Ù…ÙCstr(τpre-n), τpre-iÎXT 1； PostCon(a)=Cstr(τpost-1)Ù…ÙCstr(τpost-m),τpost-jÎXT 2。 通常情况下，嵌入式软件具有异常处理机制，以对各类运行时序异常进行处理。在ESIA模型中，对时序异常状态进行标记，以与正常状态区别描述。设P为一个ESIA 模型，定义异常状态标识v.E_tag，vÎVP，当v.E_tag值为1时，表示v为异常状态；当值为0时，表示正常状态。此外，action_E表示行为action 在异常时序下的执行分支。在action_E作用下，软件运行迁移至时序异常状态，执行相应异常处理任务。在ESIA模型中，action_E具有与action相同的触发事件，但执行效果、对应状态迁移的目标状态均不同。action_E的前置、后置条件为对action前置、后置条件中包含的变量取值约束、以及时间约束取反（取反运算符为：Ø），即若Cstr(τ1)与Cstr(τ2)分别为行为action的前置与后置条件，则ØCstr(τ1)与ØCstr(τ2)分别为异常时序分支action_E的前置与后置条件。 0r epor t!appr oachappr oach ?open1clos e2leave?clos e!leave3open!r epor t53s£τ1£7sr es et (τ1, τ2)Mod ( τ0, 15s)3s £τ1£5sr es et (τ1)r es et(τ0)r etur n;3s £τ2£30sr es et (τ0) τ0£30s4initializ atio n;τ0 = 5sopen_E ;clos e_E; 图2 具有时间约束的门禁控制软件ESIA模型. 具有时间约束的门禁控制软件ESIA模型如图2所示。其中，针对不同定时器分别定义时间变量τ0，τ1及τ2，其计时过程从置零开始，到时间约束作用点结束。每项时间变量记录了特定状态迁移序列的执行时间。如图2所示，当检测到人员抵近后，置零τ1 与τ2，τ1 记录门禁控制软件沿状态迁移序列State2→State3 执行所耗费的时间，而τ2 记录沿State2→State3→State4 执行所耗费的时间；当检测到人员离开后，再次置零τ1，并记录沿状态迁移序列State4→State1执行所耗费的时间。设定门禁控制软件的时间约束如下： DC-TR1.  系统上电后置零τ0，定义P_Cstr(τ0) = 5s (τ0 = 5s)为行为initialization;的后置条件； DC-TR2. 当检测到人员抵近事件后置零τ1 （状态2），定义D_Cstr1(τ1) = [3s, 7s]为行为open!的后置条件； DC-TR3. 当检测到人员离开事件后置零τ1 （状态4），定义D_Cstr2(τ1) = [3s, 5s]为行为close!的后置条件； DC-TR4. 当检测到人员抵近事件后置零τ2 （状态2），定义D_Cstr(τ2) = [3s, 30s]为行为leave?的后置条件； DC-TR5. 在自动门打开后置零τ0（状态3），定义D_Cstr(τ0)  = [0s, 30s]为行为close!的后置条件；   DC-TR6. 在自动门打开后置零τ0（状态3），定义C_Cstr(τ0) = 15  (Mod(τ0, 15)=0)为行为report!的前置条件。 此外，门禁系统具有一组异常时序处理机制。在运行过程中，当检测到人员抵近事件后，若打开门禁的时间超出DC-TR2 的要求（即满足ØDC-TR2），则执行异常分支open_E，门禁系统重新初始化；当检测到人员抵近事件后，若关闭门6  计算机学报  2016年 禁的时间超出DC-TR3的要求（即满足ØDC-TR3），则执行异常分支close_E，门禁系统同样重新初始化。 在本文中，认为目标软件的ESIA模型具有确定性与完整性。其中，确定性表示在相同的源状态、触发事件与时序条件下，ESIA具有唯一的后继行为；完整性表示目标系统具有的所有状态、行为、执行路径等，均在ESIA模型中予以描述，所有正确的执行片段均可映射至相应ESIA执行路径。 3.3  时间约束相关关系分析 在嵌入式软件中，一项任务的执行时间可能与其他任务相关。当不同任务的执行路径相互重叠时，如一项任务是另一项任务的子任务、或两项任务包含公共子任务时，不同任务的执行时间之间将存在特定依赖关系，造成相应时间约束之间间接相关。在时序检测中，不仅需检验各项任务的执行时间是否满足相应独立时间约束，还需检验任务的执行时间是否满足特定依赖关系，从而对软件运行时序进行充分检测。 如图2中，当检测到人员抵近事件后，时间变量τ1与τ2被同时置零并开始计时。由于与τ2关联的执行路径包含与τ1关联的执行路径，τ1与τ2之间存在取值依赖关系：τ1<τ2。若任务的执行时间违反以上依赖关系，则表示软件运行时序存在异常。 在ESIA模型中，使用ESIA执行路径Path(τ)表示与时间变量τ相关联的状态迁移序列，并对不同时间约束间的相关关系进行描述。 定义7. ESIA执行路径. P=(VP, Von P, XP, AP, YP, E, ΔP)为一个ESIA，执行路径Path(τ)定义为P之上的一个有序状态迁移子集： Path(τ)={δi | i=1,2,…,m}, Path(τ) ÍΔP，τ在δ1处置零，Cstr(τ)作用于δm； "δi，δi+1 Î Path(τ)，1 ≤ i ≤ m−1，δi 与δi+1为ESIA上两项相继的状态迁移，即δi.t = δi+1.s。 如图2 所示，Path(τ1)={State2→State3}与Path(τ2)={State2→State3,  State3→State4}即为门禁控制软件ESIA模型上的两条执行路径。 定义8.  时间约束相关关系. τ1，τ2ÎXT为ESIA上的两个时间变量，Path(τ1)与Path(τ2)为与τ1，τ2关联的执行路径，Cstr(τ1)与Cstr(τ2)之间存在以下三类相关关系： a.  相互独立(Isolated,  IR) ：若Path(τ1)∩Path(τ2)=f，则Cstr(τ1)与Cstr(τ2)相互独立； b.  包 含 相 关(Containment,  CR)：若Path(τ1)ÍPath(τ2)，则τ1与τ2之间存在取值依赖关系C_Dep(τ1, τ2)：τ1<τ2，Cstr(τ1)与Cstr(τ2)包含相关； c.  交叉相关(Overlapping, OR)：若τ1与τ2在不同 时 间 点 置 零 ， $Path(τ3)ÍΔP ，Path(τ3)=Path(τ1)∩Path(τ2)¹f，则τ1，τ2与τ3之间存在取值依赖关系O_Dep(τ1, τ2, τ3)：(τ3<τ1)˄(τ3<τ2)，Cstr(τ1)与Cstr(τ2)交叉相关； 其中，若Cstr(τ1)与Cstr(τ2)相关，则称τ1与τ2为一组相关时间变量。appr oach?1 2 3r es et(τ2)4Path (τ1)0 1 2 3Path (τ3)Path (τ2)(a) ( b)(c) ( d)δ1open ! leave? clos e !3s £ τ2 £ 30sr es et (τ1)Path (τ2)Path (τ1)3s £ τ1£ 5sappr oach ?1 2 3r es et ( τ1,τ2)4open ! leave?3s £ τ2£ 30sPath (τ2)3s £ τ1 £ 7sPath( τ1)appr oach?1 2 3r es et(τ2)4open ! leave?3s £ τ2 £ 30sPath (τ2)Path (τ0)r es et (τ0)1clos e !τ0 £30s r es et (τ1)5Cs tr ( τ1) r es et ( τ2,τ3) Cs tr ( τ2) Cs tr ( τ3) 图3: 时间约束相关关系. (a) τ1与τ2相互独立；(b) τ1与τ2包含相关；(c) τ1与τ2交叉相关；(d) τ1，τ2与τ3多重相关.  在门禁控制软件ESIA 模型中，时间约束D_Cstr(τ2)与D_Cstr2(τ1)相互独立（图3.a）；时间约束D_Cstr1(τ1)与D_Cstr(τ2)包含相关（图3.b）；时间约束D_Cstr(τ2)与D_Cstr(τ0)交叉相关（图3.c）。对相关关系的定义可扩展到多个时间变量。如图3.d所示，若$δÎΔP，且δÎ∩k i=0Path(τi)，则k个时间变量{τi |  i=1，2，…，k}之间存在相关关系。本文主要对两项时间变量相关时的时序检测方法进行讨论。当多项时间约束之间存在多重相关关系时，不同时间变量之间的取值依赖关系将更加复杂。 论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  7 4  基于相关性分析的时序缺陷检测 在时序缺陷检测过程中，根据目标软件ESIA模型描述与执行路径上的时间约束相关性分析结果，对预先提取的包含时间信息的执行片段进行离线自动检测，以检查软件在运行过程中是否存在时序异常，并检查软件的异常时序处理机制是否满足设计要求。本文将包含时间信息的执行片段定义为一个行为执行序列，以描述系列任务的执行过程。 定义9.  包含时间信息的执行片段.  包含时间信息的执行片段Trace定义为一个行为执行序列： · Trace={ λj | j=1,2,…,n}，λj 为第j 项行为的执行过程； · "λj 表示为一个六元组λj = (e, τj1=vj1, reset(τj3), a, τj2=vj2, reset(τj4))；其中，λj.e为触发行为执行的事件，λj.a为相应行为；τj1，τj2，τj3，τj4ÎXT P为四项时间变量，τj1 在行为λj.a开始时完成计时，计时时间为vj1；τj2 在行为λj.a结束时完成计时，计时时间为vj2；τj3 行为λj.a开始执行时置零并启动计时；τj4 行为λj.a执行结束时置零并启动计时。 在执行片段提取过程中，若λj 中的某项信息不存在，则相应元素空缺。若一项执行片段不包含时间信息，则无需描述与其相关联的时间变量、任务执行时间与置零行为。在TBTDD方法中，执行片段的记录应规范、完整，以便后续解析与检测。 异常时序处理机制是嵌入式软件可靠性设计与验证的重要内容。在TBTDD方法中，不仅需要对软件正常运行时序进行检测，还需要对软件异常运行时序处理机制进行检测，以避免产生非预期的结果。本文将执行片段分为正常时序片段与异常时序片段，定义如下： a. 正常时序片段：当一条执行片段仅包含正常时序与相应执行分支时，该片段为正常片段； b. 异常时序片段：当一条执行片段包含异常时序与相应异常处理分支时，该片段为异常片段。 执行片段的提取应尽可能覆盖各类正常、异常运行时序，以对目标软件时序特性进行充分检测。 TBTDD方法工作流程如图4所示。 执行片段可接受性准则时序缺陷离线检测执行片段匹配相关时间约束识别时序特性可满足性准则测试资产库时序检测过程ESIA模型描述时序特性验证2 3 4执行片段提取15目标软件执行片段提取规范图4 TBTDD方法工作流程 1.  执行片段提取与预处理。在目标软件运行环境中，通过在目标机、周边设备、仿真设备上设置观察点或探针，实时记录软件运行过程中的触发事件、任务执行序列、执行时间、及启动计时等时间信息，按照记录规范对其进行处理后，组织构建执行片段并存入软件运行日志。 2.  执行片段匹配。依据执行片段可接受性准则，为每条执行片段选取匹配的ESIA执行路径；针对无法匹配的执行片段，报告软件运行异常，并判断缺陷类型。 3.  相关时间约束识别。在每条匹配的ESIA执行路径上，识别各项独立、相关时间约束，提取不同时间变量间的取值依赖关系。 4.  时序缺陷检测。依据时序特性可满足性准则，检查执行片段包含的时间信息是否满足匹配路径上各项独立、相关时间约束的要求，检查软件异常时序处理机制是否满足设计要求，检测软件缺陷并识别缺陷类型。 5.  时序特性验证。根据时序特性检测结果，验证目标软件时序特性是否满足设计要求。 4.1  执行片段匹配 若执行片段包含的行为序列与特定ESIA执行路径相匹配，则称该执行片段可被目标软件ESIA模型接受。本节制定执行片段可接受性准则，依据该准则，提出一种广度优先候选状态算法，对特定执行片段上的每项行为进行逐项匹配，在目标软件ESIA模型之上搜索与其相匹配的ESIA执行路径，并滤除ESIA无法接受的执行片段。由于目标软件ESIA模型包含各类正常、异常时序分支，以下执行片段可接受性准则与匹配算法同时适用于正常时序片段与异常时序片段的匹配过程。 执行片段可接受性准则定义如下。 定义10.  执行片段可接受性. P=(VP, Von P, XP, AP, YP,  E,  ΔP)为一个ESIA，执行片段Trace  =  {  λj  | j=1,2,…,n}可被P接受，当且仅当： 8  计算机学报  2016年 1) "λj =(e, τj1=vj1, reset(τj3), a, τj2=vj2, reset(τj4))，$δiÎΔP，λj.e=δi.e且λj.a=δi.a；当满足以上条件时，称λj 与δi 之间相匹配，记为δi=map(λj)； 2) "λj，λj+1ÎTrace，1 ≤ j ≤ n−1，$δi，δi+1ÎΔP，δi=map(λj)且δi+1=map(λj+1)，δi.t=δi+1.s，即δi 与δi+1为ESIA上两项相继的状态迁移。 设Trace  =  {λj|  j=1,  2,…,n}为一条执行片段，VP={0, 1,…,m}为被测软件ESIA模型P的初始候选状态集合，基于可接受性准则的执行片段匹配过程包含以下步骤： 1) 从λ1开始，以VP为初始候选状态集合，启动Trace的匹配过程。 2) 在对λj 进行匹配的过程中，以一项当前候选状态为源状态，若在其上存在与λj 相匹配的状态迁移，则记录该状态迁移与对应目标状态；在所有当前候选状态之上执行以上匹配过程，并利用记录的目标状态集合更新当前候选状态集合，λj 匹配过程完成； 3) 沿执行片段Trace持续执行步骤“2）”，若Trace上的所有行为执行均正确匹配，则搜索到一组与Trace相匹配的ESIA执行路径；若特定行为无法匹配，则匹配过程终止。 设Trace={λ1，λ2，λ3}为一条执行片段，VP ={0, 1,  2,  3}为被测软件ESIA模型的初始候选状态集合，Trace的匹配过程如图5.a所示。其中，λj 对应的虚线表示对Trace上的第j 项行为进行匹配的过程，λj 对应的虚线下的一组状态表示当前候选状态集合，将在其上搜索与λj 相匹配的状态迁移。首先，对λ1进行匹配，初始候选状态集合为{0,  1,  2,  3}，若在候选状态0、2、3之上存在与λ1相匹配的状态迁移，且对应目标状态为1、0、2，则记录相应状态迁移“State0→State1”、“State2→State0”、“State3→State2”，更新当前候选状态集合为{1, 0, 2,}；随后，对λ2进行匹配，若在候选状态1、0之上存在与λ2相匹配的状态迁移，且对应目标状态为2、1，则记录相应状态迁移“State1→State2”、“State0→State1”，更新当前候选状态集合为{2, 1}；最后，对λ3进行匹配，若在候选状态1之上存在与λ3相匹配的状态迁移，且对应目标状态为3，则记录相应状态迁移“State1→State3”，执行片段匹配完成，搜索得到的匹配路径为{State2→State0, State0→State1, State1→State3}。0 2 1 31 0322 10 2 1 31 0322 1(a) ( b)λ1 λ2 λ3 λ1 λ2 λ3 0 2 1 31 0232 1(c)λ1 λ2 λ3 3 图5 执行片段匹配过程  在一条执行片段的匹配过程中，由于一项行为可能与多个候选状态上的特定状态迁移相匹配，因而可能存在多条与其相匹配的ESIA执行路径。如图5.b、5.c所示，在被测软件ESIA模型之上均存在3条与Trace={λ1，λ2，λ3}相匹配的执行路径。 例如在图2所示的门禁控制软件中，提取执行片段Trace  = {(man  approach,  ,  ,  approach?,  , reset(τ1, τ2)), ( , , , open!, D_Cstr1(τ1), reset(τ0)), (man leave, , , leave?, D_Cstr(τ2), reset(τ1)), ( , , , close!, D_Cstr2(τ1)ÙD_Cstr(τ0), )}。通过执行片段匹配，在门禁控制软件ESIA模型中搜索得到的匹配路径为Path={State1→State2,State2→State3, State3→State4, State4→State1}。 当存在多条与执行片段相匹配的ESIA执行路径时，若不同的匹配路径具有不同的时间约束，则无法唯一确定执行片段应满足的时序设计要求。在此情况下，针对所有匹配路径进行相关时间约束识别与时序缺陷检测，若执行片段包含的时间信息无法满足所有匹配路径的时序要求，则软件运行时序异常，需对其作进一步分析。此外，若不存在与执行片段相匹配的ESIA执行路径，则将该执行片段过滤，不再对其进行时序缺陷检测。在此情况下，软件实现可能具有ESIA模型未描述的运行场景，或可能存在功能性缺陷，需对提取的执行片段与相应功能设计要求进行进一步检查，但不能确定软件实现是否存在时序缺陷。 执行片段匹配算法具体定义如下。 算法1.  执行片段匹配Trace_Match( ). 输入:  A  Trace={λj|  j=1,2,…,n}  and  ESIA  P 输出:  A  set  of  matched  execution  path  (SMEP) 论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  9 数据结构:  Current  candidate  states (CCS)  Trace_Match(Trace, P) BEGIN CCS=VP FOR  each  q  in  CCS  //初始化SMEP Create  an  execution  path  for  state  q END  FOR FOR  each  λ  on  Trace  //检测每一项行为执行 λpre is the precursor action of λ on Trace δpre=map(λpre), δpreÎΔP FOR  each  q  in  CCS  //检测每一项候选状态 IF($δÎΔP,  δ=map(λ)  and δ.s=δpre.t) Add δ  to  corresponding  path  in  SMEP Replace q  by q’  in  CCS ELSE Remove  corresponding  path  from  SMEP Remove q  from  CCS END  FOR Remove  redundant  states  from  CCS IF(CCS=f) //执行片段不可接受 Return  No-Matching ELSE Null END  FOR Return SMEP END 在以上算法中，设n为执行片段长度，m为候选状态集合包含的状态数，则算法复杂度为O(n´m)。执行片段长度、ESIA模型规模、特定行为在ESIA模型中的出现频度等因素都将影响匹配结果与效率。因此，通过制定执行片段提取规范，控制执行片段的起点、终点、结构与长度，可改善算法的执行效率。 4.1.1  模型覆盖率 嵌入式软件在不同外部事件触发下，往往具有大量执行序列，难以进行完全检测。本文利用匹配路径集对ESIA模型的覆盖率衡量时序特性检测的充分性。 本文采用的ESIA模型覆盖准则如下： a.  状态覆盖：执行路径集应覆盖ESIA中的所有状态；设ns为ESIA总状态数，ms为执行路径集覆盖的状态数，状态覆盖率StatesCvr计算如下： 100%ssmStatesCvrn=´                                （1） b.  迁移覆盖：执行路径集应覆盖ESIA中的所有状态迁移；设nt 为ESIA总状态迁移数，mt 为执行路径集覆盖的状态迁移数，状态迁移覆盖率TransitionsCvr计算如下： 100%ttmTransitionsCvrn=´                   （2） c.  循环覆盖：在任意一条执行路径之上，对ESIA 中每一项循环结构的遍历不超过n 次（All-Loop-n），且路径包含的循环结构数不超过m（All-m-Loop）；执行路径集应覆盖ESIA中所有满足以上要求的路径；设nl 为ESIA总循环结构数，ml 为执行路径集覆盖的循环结构数，循环覆盖率LoopsCvr计算如下： 100%llmLoopsCvrn=´                                （3） d.  独立时间约束覆盖：执行路径集应覆盖ESIA中的所有独立时间约束；设nitc 为ESIA总独立时间约束数，mitc 为执行路径集覆盖的独立时间约束数，独立时间约束覆盖率ITConstraintsCvr 计算如下： int 100%itcitcmITConstra sCvrn=´            （4） e. 相关时间约束覆盖：执行路径集应覆盖ESIA中的所有相关时间约束；设nrtc为ESIA总相关时间约束数，mrtc 为执行路径集覆盖的相关时间约束数，相关时间约束覆盖率RTConstraintsCvr计算如下： int 100%rtcrtcmRTConstra sCvrn=´           （5） 当匹配路径集满足以上覆盖准则时，认为执行片段提取、以及时序缺陷检测工作已足够充分。 4.2  相关时间约束识别 为检验执行片段包含的时间信息是否满足各项独立、相关时间约束要求，需在每条匹配的ESIA执行路径之上，识别其包含的相关时间约束。每项相关时间约束定义为一个三元组R_Cstr=(XT,  YT, type)，其中，XT表示一组时间变量；YT表示XT中的时间变量具有的一组时间约束；type 表示YT中的时间约束具有的相关关系类型，可以是包含相关（CR）、交叉相关（OR）等。 10  计算机学报  2016年 时间约束限制特定任务的执行时间。在嵌入式软件中，通过时间变量的计时过程记录特定任务的执行时间，其计时过程从任务启动时开始，到任务完成或异常终止时结束。因此，一项时间变量τ的计时区间与关联任务执行路径Path(τ)之间完全重合。在相关时间约束识别过程中，通过分析不同时间变量计时区间的重叠情况，判断相应任务执行路径之间的重叠方式，进而根据前述相关关系定义，确定不同时间变量之间存在的取值依赖关系，识别相应时间约束之间存在的相关关系。 本文采用时间约束相关矩阵进行时间约束间的相关关系判断。通过遍历特定匹配路径，搜索不同时间变量的计时起点、计时终点（即时间约束作用点），动态构建与更新相关矩阵。在时间变量的计时起点，将其添加至相关矩阵；在时间变量的计时终点，将其从相关矩阵中移除，并对相应时间约束的相关性进行分析与判断，具体判断准则如下： ·  若一项时间变量所属列具有前列，或者同列中包含多项时间变量，则相应时间约束之间包含相关； ·  若一项时间变量所属列具有后列，则相应时间约束之间交叉相关； ·  若两项时间变量同时结束计时，则相应时间约束之间包含相关。 设Path ={δ1, δ2, δ3, δ4}为一条ESIA执行路径，τ1、τ2、τ3、τ4为与Path相关联的四项时间变量。其中，τ1在δ1.a开始时置零，τ2、τ3在δ1.a结束时置零，τ4 在δ2.a 开始时置零；Cstr(τ3)Îδ2.PostCon，Cstr(τ1)Îδ3.PreCon ， Cstr(τ2)Îδ3.PostCon ，Cstr(τ4)Îδ4.PostCon。Path之上的相关矩阵动态构建与相关时间约束识别过程如下所示： ( )1t (1.a) 123tttæö Þç÷-èø (1.b) 1 2 43t t ttæö Þç÷-- èø (1.c) ( )1 2 4t t t Þ (1.d) ( )24 tt Þ (1.e) ( )4t Þ (1.f) 当沿路径Path遍历至δ1.a开始位置时，时间变量τ1开始计时，在时间约束相关矩阵中新建一列，将τ1添加至该列（步骤1.a）；在δ1.a结束位置，时间变量τ2、τ3开始计时，将τ2、τ3添加至相关矩阵新建列（步骤1.b）；在δ2.a开始位置，时间变量τ4开始计时，将τ4添加至相关矩阵新建列（步骤1.c）；在δ2.a结束位置，时间变量τ3结束计时（即Cstr(τ3)作用点），对Cstr(τ3)与其他时间约束之间的相关性进行判断，识别出Cstr(τ3)分别与Cstr(τ1)、Cstr(τ2)包含相关，与Cstr(τ4)交叉相关，并将τ3从相关矩阵中移除（步骤1.d）；继续执行后续步骤(步骤1.e与1.f)，识别出Cstr(τ1)分别与Cstr(τ2)、Cstr(τ4)交叉相关，Cstr(τ2)与Cstr(τ4)交叉相关。 例如在图2所示的门禁控制软件ESIA模型中，Path={State1→State2,State2→State3, State3→State4, State4→State1}为一条匹配路径，τ0、τ1、τ2为与Path相关联的三项时间变量。Path之上的相关矩阵动态构建与相关时间约束识别过程如下所示： 12ttæöç÷èø (2.a) ( )20 tt Þ (2.b) ( )01 tt Þ (2.c) 当沿路径Path遍历至approach结束位置时，时间变量τ1、τ2开始计时，在时间约束相关矩阵中新建一列，将τ1、τ2添加至该列（步骤2.a）；在open结束位置，时间变量τ1结束计时（即D_Cstr1(τ1)作用点），识别出D_Cstr1(τ1)与D_Cstr(τ2)包含相关，并将τ1从相关矩阵中移除，时间变量τ0开始计时，将τ0添加至相关矩阵新建列（步骤2.b）；在leave结束位置，时间变量τ2结束计时（即D_Cstr(τ2)作用点），识别出D_Cstr(τ2)与D_Cstr(τ0)交叉相关，并将τ2从相关矩阵中移除，时间变量τ1重新开始计时，将τ1添加至相关矩阵新建列（步骤2.c）；在close结束位置，时间变量τ0、τ1结束计时（即D_Cstr(τ0)、D_Cstr2(τ1)作用点），识别出D_Cstr(τ0)与D_Cstr2(τ1)包含相关，并将τ0、τ1从相关矩阵中移除。 由此，在门禁控制软件的匹配路径Path之上，识别出的相关时间约束如下： R_Cstr1=({τ1, τ2},{D_Cstr1(τ1),D_Cstr(τ2)}, CR)； R_Cstr2=({τ2, τ0}, {D_Cstr(τ2), D_Cstr(τ0)}, OR)； R_Cstr3=({τ0, τ1}, D_Cstr(τ0), D_Cstr2(τ1)}, CR)。 相关时间约束识别算法具体定义如下。 算法2.  相关时间约束识别Correlation_Identify( ). 输入:  An  ESIA Path={δi|  i=1,2,…,m} 输出:  A  set  of  correlated  timing  constraints(SCTC) 论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  11 数据结构:  Timing  constraints  matrix (TCM)  Correlation_Identify(Path) BEGIN FOR  each  δ  on Path IF($τ reset  at  the beginning  of δ) Create  a  column  c  in  TCM FOR  each  τ  reset  at  the beginning  of δ Add τ  to  c IF($Cstr(τ)Îδ.PreCon) Identify(δ.PreCon)  //识别相关时间约束 IF($τ reset  at  the  end  of  δ)   Create  a  column  c  in  TCM FOR  each  τ  reset  at  the  end  of δi Add τ  to  c IF($Cstr(τ)Îδ.PostCon) Identify(δ.PostCon)  //识别相关时间约束 END FOR END  Identify(A  set  of  timing  constraints(STC)) BEGIN FOR  each  Cstr(τ)  in  STC Get  the  column  number  cn  of τ  in  TCM Get  the  line  number  ln  of  τ  in  TCM IF($R_CstrÎSCTC  and τÎR_Cstr.XT)  //已识别的相关时间约束 Add  Cstr(τ)  to  R_Cstr.YT END  IF IF(0<cn)  //所属列具有前列 FOR  each τpre  in  pre-columns in  TCM Create R_Cstr，  R_Cstr.XT={τpre,  τ}，  R_Cstr.type=CR add R_Cstr  to  SCTC END  IF IF(0<ln)  //同列中包含多项时间变量 FOR  each τpre  in  same-column  in  TCM   Create R_Cstr，  R_Cstr.XT={τpre,  τ}，  R_Cstr.type=CR add R_Cstr  to  SCTC END  IF IF(cn+1<the  number  of  column  in  TCM))  //所属列具有后列 FOR  each τpost  in  post-columns in TCM Create R_Cstr，R_Cstr.XT={τ,  τpost}，  R_Cstr.type=OR add R_Cstr  to  SCTC END  IF Remove τ from TCM END FOR END 在以上算法中，设n为执行路径长度，m为特定行为前置、后置条件中包含的时间约束数，l1、l2与l3分别为相关矩阵中特定时间变量前列、同列与后列包含的时间变量数，则算法复杂度为O(n´m´(l1+l2+l3))。 4.3  时序缺陷分析 嵌入式软件故障管理主要包括五个方面，分别是故障检测、故障定位、故障隔离、系统重构、故障修复等[7-8]。本文主要关注对目标软件中存在的单一时序故障进行检测、识别与定位。当目标软件中同时存在多重时序故障时，时序缺陷的检测、定位将更加复杂，且由于不同故障间的相互作用，软件运行过程中的时序异常可能被掩盖。 本节对嵌入式软件运行过程中可能出现的功能、时序异常进行分析，确定执行片段中可能存在的时序缺陷类型，作为制定时序特性检测准则的基础，有针对性的指导时序异常检测、缺陷识别工作。 在目标软件ESIA模型之上，若不存在与执行片段相匹配的ESIA执行路径，则软件实现存在功能性缺陷。Miller、Alcalde等将执行序列检测过程中出现的功能异常分为输出故障与状态迁移故障[9-10]。其中，输出故障描述在特定源状态与行为作用下，软件运行产生不符合预期的输出；状态迁移故障描述在特定源状态与行为作用下，软件运行迁移至不符合预期的目标状态。在本文中，根据执行片段可接受性准则，软件运行过程中可能存在的功能异常如下： ·  行为错配（违反准则定义10.1）。针对执行片段上的特定行为，无法在ESIA模型之上搜索到匹配的状态迁移，具体包括：触发事件匹配错误，行为执行匹配错误等。 ·  行为错序（违反准则定义10.2）。针对执行片段上的两项相继行为，无法在ESIA模型之上搜索到匹配的相继状态迁移，具体包括：两项状态迁移的前驱/后继关系错误，两项状态迁移不是相继的状态迁移等。 在TBTDD方法中，若不存在与执行片段相匹12  计算机学报  2016年 配的ESIA执行路径，则识别并报告软件存在的功能性缺陷，并通过进一步核查确定该缺陷属于软件实现缺陷或设计缺陷。 嵌入式软件运行过程中可能存在的时序异常如下： ·  违反独立时间约束。一项时间变量的取值违反特定时间约束，或在匹配的状态迁移之上未搜索到对应的时间约束。 ·  违反相关时间约束。一组时间变量的取值违反特定时间约束间相关关系。 ·  违反计时起点要求。特定时间变量的计时起点与设计要求不符。 ·  异常时序处理错误。针对特定异常时序的处理机制与设计要求不符。 其中，对于时间点约束，若预期事件在规定的时间点没有产生，则软件运行时序异常；对于持续时间约束，若任务执行时间低于下限阈值、或高于上限阈值，则运行时序异常；而对于周期时间约束，若任务重复执行的时间间隔不满足周期时间要求，则运行时序异常。 时间约束间相关关系由执行路径上不同任务间的关联方式引起，是软件运行过程中必须遵循的物理规律。在正确实现的目标软件中，不会存在违反相关时间约束的执行时间；而在错误实现的目标软件中，则可能存在此类异常时序。在传统时序测试过程中，若针对此类异常时序设计测试用例，当软件实现正确时，其将为无效用例，无法在目标系统中配置与执行，或由于执行错误而产生错误的测试结果；若不设计此类用例，则难以发现违反相关关系的异常时序。在TBTDD方法中，通过观察目标软件运行情况，对其中包含的时间信息进行检测，以验证软件运行时序是否正确，从而避免了以上问题，为此类异常时序的检测提供了新的有效手段。 此外，不安全的异常时序处理方式同样会造成软件运行状态异常。在传统时序测试过程中，一般通过人工设置违反时间约束要求的运行时间，以观察软件时序异常处理机制是否满足设计要求。在此过程中，不仅难以完全覆盖软件运行过程中的各类异常时序，且难以模拟特定环境条件下的偶发异常时序。在TBTDD方法中，通过长期监控目标软件运行，提取充分的执行片段集合并进行检测，可有效发现此类影响目标软件运行可靠性的潜在缺陷，甚至侦测到多余的软件运行分支。 4.4  时序缺陷检测 在时序特性检测过程中，通常需要制定一组检测准则，当执行片段包含的时间信息满足检测准则时，即认为软件运行时序满足设计要求。在TBTDD方法中，根据时序缺陷类型分析，制定时序特性可满足性准则，并利用ESIA模型描述的时间需求作为检测度量，对执行片段包含的时间信息与异常时序处理机制进行检测。其中，通过对异常时序处理机制进行检测，可有效保证嵌入式软件运行的健壮性与可靠性。以下时序特性可满足性准则与时序缺陷检测算法同时适用于正常时序片段与异常时序片段的检测过程。 时序特性可满足性准则定义如下。 定义11.  时序特性可满足性. P为一个ESIA，执行片段Trace = {λj| j=1,2,…,n}可被P接受，匹配路径为Path ={δi| i=1,2,…,n }，执行片段包含的时间信息满足ESIA时序特性要求，当且仅当"λj  = (e, τj1=vj1, reset(τj3), a, τj2=vj2, reset(τj4))及δi =map(λj)： 1)  对于τj1 ，$Cstr(τj1)Îδi.PreCon，且vj1⊢Cstr(τi1)；对τj2 ，$Cstr(τj2)Îδi.PostCon，且vj2⊢Cstr(τj2)； 2) 若$R_Cstr，R_Cstr.XT={τj1, τx}，τxÎXT P，则vj1⊢Dep(τj1, τx)；若$R_Cstr，R_Cstr.XT={τj2, τy}，τyÎXT P，则vj1⊢Dep(τj2, τy)；若$R_Cstr，R_Cstr.XT={τj1, τj2}，则vj1⊢Dep(τj1, τj2)且vj2⊢Dep(τj1, τj2)； 3) τj3在行为δi.a开始时置零；τj4在行为δi.a结束时置零。 在时序缺陷检测过程中，依据可满足性准则，对执行片段上的各项行为进行逐项检查，检测其包含的时间信息是否满足匹配路径上相应独立、相关时间约束的要求，检测并识别不同类型的软件时序缺陷。其中，对于一组相关时间约束，在后结束计时的时间变量的计时终点，对两项相关时间变量间的取值依赖关系进行检测。 例如在图2所示的门禁控制软件中，执行片段为Trace = {(man  approach, , , approach?,  , reset(τ1, τ2)), ( , , , open!, D_Cstr1(τ1), reset(τ0)), (man leave, , , leave?,  D_Cstr(τ2),  reset(τ1)),  (  ,  ,  ,  close!, D_Cstr2(τ1)ÙD_Cstr(τ0), )}，匹配的ESIA执行路径为Path  ={State1→State2,  State2→State3,  State3→State4, State4→State1}，识别的相关时间约束如4.2节所述（R_Cstr1、R_Cstr2、R_Cstr3）。该执行片段的时序缺陷检测过程为：针对行为approach?，检测τ1、τ2是否在该行为结束时置零；针对行为open!，论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  13 检测τ1的计时时间是否满足D_Cstr1(τ1)的要求，检测τ0是否在该行为结束时置零；针对行为leave?，检测τ2的计时时间是否满足D_Cstr(τ2)的要求，检测τ1、τ2的计时时间是否满足R_Cstr1的要求，检测τ1 是否在该行为结束时置零；针对行为close!，检测τ1的计时时间是否满足D_Cstr2(τ1)的要求，检测τ0的计时时间是否满足D_Cstr(τ0)的要求，检测τ2、τ0的计时时间是否满足R_Cstr2的要求，检测τ0、τ1的计时时间是否满足R_Cstr3的要求。 时序缺陷检测算法具体定义如下。 算法3.    时序缺陷检测Defect_Detection( ). 输入:  A  Trace={λj|  j=1,2,…,n} A  matched  Path={δi|  i=1,2,…,n}  on  ESIA  P A  set  of  correlated  timing  constraints(SCTC) 输出:  The  result  of  defect  detection (RDD)  Defect_Detection(Trace,  Path,  SCTC) RDD=FALSE BEGIN FOR  each λ  on  Trace Get δ=map(λ)  on  Path FOR  each time  value τ=v  record  before  or  after  the  execution  of λ.a IF(  ($Cstr(τ)Îδ.PreCon  AND  v⊢Cstr(τ))  OR  ($Cstr(τ)Îδ.PostCon  AND  v⊢Cstr(τ)) )  //独立时间约束检测 Null ELSE TDR=Constraint_voliation Return  RDD IF($R_CstrÎSCTC,  R_Cstr.XT={τ,  τx},τxÎXT P  AND  v⊢Dep(τ,  τx)  //相关时间约束检测 Null ELSE TDR=Correlation_voliation Return  TDR END  FOR FOR  each  τ  reset  at  the beginning  OR  end  of λ//计时起点检测 IF(τ  is  reset  at corresponding  location  of δ)  //置零行为检测 Null ELSE RDD=Reset_Error Return  RDD END  FOR END  FOR END 在以上算法中，设n为执行片段长度，m1为行为开始或结束时采集的执行时间的组数，m2为行为开始或结束时置零的时间变量数，则算法复杂度为O(n´m1+ n´m2)。 在时序缺陷检测过程中，针对每一条执行片段，依次调用以上执行片段匹配、相关时间约束识别、以及时序缺陷检测算法，得到相应检测结果。此外，在TBTDD方法中，可根据匹配的ESIA执行路径对时序缺陷进行定位。当软件运行时序违反特定时间约束、相关关系、计时起点设置时，或者特定时序异常处理机制与设计要求不符时，软件实现的对应部分可能存在缺陷。 5  实验与评估 本文设计实现了ATES(Automated Test Platform for Embeded Software)平台原型系统，内建TBTDD时序检测方法，支持嵌入式软件时序特性建模与离线自动检测，识别与管理各类时序故障，平台架构如图6所示。 ATES平台具有以下功能： a)  基于ESIA模型的嵌入式软件时序特性建模； b) 基于可接受性准则的执行片段匹配； c)  基于相关矩阵的相关时间约束识别； d)  检测软件运行时序，侦测执行片段中的时序异常，验证异常时序处理机制的有效性，发现并识别各类软件时序缺陷； e)  针对执行片段集制定检测计划，管理并报告时序故障。 支持层ES IA 模型公共应用应用层时序特性建模 时序特性检测时序特性检测准则测试计划故障管理执行片段匹配相关时间约束识别时序缺陷检测基础层执行片段可接受性准则执行片段记录规范 图6 ATES平台架构 在实验过程中，利用ATES平台提供的基础类，人工编写被测软件的ESIA模型代码，对其时序特性进行定量描述；进而在ATES平台上，以ESIA14  计算机学报  2016年 模型为基础模型，调用平台内建的TBTDD方法，对预先提取的执行片段集执行时序检测。在ATES平台之上，测试人员可灵活制定测试计划，组织调用各项平台功能，并动态监控检测过程。 5.1  实验设计 本节以一项卫星定位系统软件(Satellite  Positioning  System  Software,  SPS)为例，对ESIA时序语义与TBTDD方法进行验证与评估。 5.1.1   目标软件建模 卫星定位导航指利用导航卫星信号对地面、空中、空间、海洋目标进行定位、导航的技术，通过测量平台与多颗导航卫星之间的距离，并综合卫星位置数据等信息，精确计算平台所处位置，引导其沿既定路线行进。当前，卫星定位导航技术已在地面车辆、航空、航天、航海、地理数据采集、以及高精度测量等领域得到广泛应用。美、俄、欧洲、中国等国家或地区均已建立、或正在建立各自主导的全球性卫星导航系统，如美国的全球定位系统(Navigation  Satellite  Timing  And  Ranging  Global  Positioning  System，GPS)、俄罗斯的格洛纳斯系统(Global  Navigation  Satellite  System，GLONASS)、欧洲的伽利略系统(Galileo  Positioning  System，Galileo)、以及中国的北斗卫星导航系统(BeiDou  Navigation  Satellite  System，BDS)等，目标均是实现全球范围内的连续、实时、高精度、全天候定位与导航。为保证定位的精度与实时性，各类卫星定位系统均具有严格的时间性能要求。 本节中的卫星定位系统软件利用BDS卫星信号，实时完成定位解算，向用户提供平台位置、速度等信息。SPS软件是典型的实时嵌入式软件，直接运行于板级支持包(Board Support Package，BSP)与嵌入式处理器平台之上，并通过各类总线与系统内的其他嵌入式设备连接。 SPS软件既可利用BDS普通测距码(C码)进行定位解算，也可利用精密测距码(P码)进行定位解算。在利用P码进行定位解算时，其具有M1、M2两种P码接收方式。由此，SPS软件具有C、P-M1、以及P-M2三种定位解算模式。此外，SPS软件具有S1、S2两个工作阶段，在不同工作阶段内，根据运行时间信息，依据特定切换策略，交替采用以上三种解算模式，以进行持续、可靠的定位与导航。 · S1阶段：在此阶段内，SPS软件首先进入P-M1模式，若在规定时间内未接收到BDS卫星信号，则切换至P-M2模式； · S2阶段：SPS软件可能在P-M1、或P-M2两种模式下由S1阶段转入S2阶段，在此情况下，其在S2阶段内具有不同的定位解算模式切换策略，导致以下不同的工作场景： —S2_M1：SPS软件首先进入P-M1模式，若在规定时间内未接收到BDS卫星信号、或在规定时间内未完成定位解算，则在P-M2、C模式之间顺序切换； —S2_M2：SPS软件首先进入P-M2模式，若在规定时间内未接收到BDS卫星信号、或在规定时间内未完成定位解算，则在P-M1、C、P-M2模式之间循环切换。 SPS软件具有以下时间需求： SPS-TR1.  在P-M1模式下，应在时间区间[t1-1, tu-1]内接收卫星信号； SPS-TR2. 在C、P-M1与P-M2模式下，应在时间区间[t1-2, tu-2]内完成定位解算； SPS-TR3. 在C、P-M2模式下，应在时间区间[t1-3, tu-3]内接收卫星信号。 0Rcv_M 1InfRcv_M1Inf?1Ret_InfCapP_M 1?CapP_M 1tl - 1 <  τ1  < tu -132r es et(τ1) ;CapP_M 2?CapC?4CapP_M 1_E ;Ret_Inf !CapP_M 2CapC5Ret_ExcInf!Ret_ExcInfr es et ( τ1) ;Ret _Inf! 图7-(a) SPS_S1模型 论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  15 0Ret_ Pos InfCapP_M1?CapP_M1? tl- 1  <  τ1  < tu -131 2r es et(τ1 ,τ2) Exe_Pos ; tl - 2  < τ2  <  tu- 26CapP_ M2?4 tl- 3  <  τ3  <  tu - 35Exe_Pos ; tl- 2  <  τ2  <  tu- 2CapP_M 1_E;Exe _Pos _E;CapP_M2 _E;Exe _Pos _E;7CapC?CapC_E;8Exe _Pos ; tl - 2  < τ2  <  tu- 2 tl - 3  < τ3  <  tu- 3Exe_ Pos_E;Ret_Pos Inf!Ret_Pos Inf!Ret _Pos Inf!r es et(τ3 ,τ2)r es et(τ3,τ2)r es et(τ3 ,τ2)r es et(τ3 ,τ2)CapP_M2? CapC?9Ret_ ExcInf!11Ret _ExcInf!r es et(τ3 ,τ2)10Ret _ExcInf!Ret_ExcInfr es et(τ1 ,τ2)     3CapP_M1?CapP_M1? tl -1  <  τ1  < tu- 124 5r es et(τ3 ,τ2)Exe _Pos ; tl - 2  < τ2  <  tu- 26CapP_M2?1 tl-3  < τ3  < tu - 30Exe_Pos ; tl- 2  <  τ2  < tu -2CapP_M1_ E; Exe _Pos _E;CapP_M2_E;Exe_Pos _E;7CapC?CapC_E;Exe _Pos ; tl- 2  <  τ2  < tu - 2 tl - 3  < τ3  <  tu- 3Exe_ Pos _E;Ret_Pos Inf!Ret_Pos Inf!Ret_Pos Inf!r es et(τ3 ,τ2)r es et(τ3,τ2)r es et(τ3,τ2)r es et(τ1 ,τ2)CapP_M2?CapC?Ret _ExcInf!8Ret _ExcInf!r es et(τ3 ,τ2)910Ret_ExcInf!r es et(τ1 ,τ2)11Ret_ Pos Inf Ret_ExcInf 图7-(b) SPS_S2_M1模型                             图7-(c) SPS_S2_M2模型 SPS软件在S1、S2阶段下的ESIA模型如图7所示。其中，Rcv_M1Inf行为接收P码初始装订信息；Ret_Inf行为返回卫星导航数据；CapP_M1、CapP_M2与CapC行为分别采用M1模式接收P码、采用M2模式接收P码、以及接收C码；Exe_Pos行为在相应模式下执行定位解算；Ret_PosInf行为返回定位结果；Ret_ExcInf行为返回异常信息。其中，action_E表示行为action的异常执行分支，引导软件进入相应异常处理。 在SPS软件运行的S1阶段（如图7.a 所示），首先进入P-M1模式，Rcv_M1Inf接收P码初始装订信息，引导CapP_M1接收P码，由Ret_Inf向用户返回接收到的导航信息。若在规定时间内未接收到P码，则转入异常分支CapP_M1_E，由Ret_ExcInf返回异常信息，SPS软件切换至P-M2模式。在P-M2模式下，CapC接收C码，进而引导CapP_M2接收P码，并由Ret_Inf返回导航信息。 在SPS软件运行的S2_M1阶段（如图7.b 所示），首先进入P-M1模式，CapP_M1接收P码，Exe_Pos执行定位解算，由Ret_PosInf返回定位结果。若在规定时间内未接收到P码，或在规定时间内未完成定位解算，则分别转入异常分支CapP_M1_E、Exe_Pos_E，由Ret_ExcInf返回异常信息，SPS软件切换至P-M2模式。在P-M2模式下，CapP_M2接收P码，Exe_Pos执行定位解算，由Ret_PosInf返回定位结果。若在规定时间内未接收到P码，或在规定时间内未完成定位解算，则分别转入异常分支CapP_M2_E、Exe_Pos_E，由Ret_ExcInf返回异常信息，SPS软件切换至C模式。在C模式下，CapC接收C码，Exe_Pos执行定位解算，由Ret_PosInf返回定位结果。若在规定时间内未接收到C码，或在规定时间内未完成定位解算，则分别转入异常分支CapC_E、Exe_Pos_E，由Ret_ExcInf返回异常信息，SPS软件再次切换至P-M2模式。 SPS软件运行的S2_M2阶段（如图7.c 所示）与S2_M1阶段相似，区别在于SPS软件将首先进入P-M2模式，并在P-M2模式、P-M1模式、C模式之间循环切换。 τ1，τ2与τ3为三项时间变量，在SPS软件不同运行阶段模型中，τ1记录P-M1模式下的卫星信号接收时间，τ2记录C、P-M1与P-M2模式下的定位解算时间，τ3记录C、P-M2模式下的卫星信号接收时间。 根据SPS软件的时间需求，设置其时间约束如下： SPS-TR1. D_Cstr(τ1) = [t1-1, tu-1]； SPS-TR2. D_Cstr(τ2) = [t1-2, tu-2]； SPS-TR3. D_Cstr(τ3) = [t1-3, tu-3]。 在以上时间约束之间，存在以下相关关系： · Path(τ1)ÍPath(τ2)，D_Cstr(τ1)与D_Cstr(τ2)包含相关，C_Dep(τ1, τ2)：τ1 < τ2； · Path(τ3)ÍPath(τ2)，D_Cstr(τ3)与D_Cstr(τ2)包含相关，C_Dep(τ3, τ2)：τ3 < τ2。 5.1.2   执行片段提取 执行片段提取工作在面向目标机的半实物仿真环境中进行。在各类运行场景下，采用预先制定的信息标识，在软件运行日志中，按规定格式实时记录软件执行序列与相应时间信息，提取有限的执16  计算机学报  2016年 行片段集，作为离线时序检测的输入数据。 嵌入式软件运行日志保存一系列软件运行时信息，为后续的运行结果分析、故障管理、任务回放与系统维护等提供数据支持。在软件运行过程中，将提取的执行片段实时保存在运行日志中，并可通过目标机调试接口进行调阅。 执行片段的提取需要遵循一定规范，以使获得的执行片段具有相同规格，为后续集中、统一处理提供便利。在实验过程中，采用的执行片段提取规范如下： 1) 起点要求：在S1阶段，以上电初始状态为执行片段记录起点；在S2阶段，以转入S2阶段的初始状态为记录起点； 2) 终点要求：从记录起点开始，当软件运行终止（当前状态无后继行为）、或软件运行回到相应阶段的初始状态时，则执行片段记录终止； 3) 循环结构要求：从记录起点开始，当软件中循环结构的执行违反前述循环覆盖All-Loop-n /All-m-Loop准则时，执行片段记录终止； 4) 长度要求：当执行片段长度增长至len 时，lenÎZ+，执行片段记录终止。 其中，n，m与len 的取值可根据软件规模、复杂度、以及特定检测要求具体确定。在本节中，设置n与m的取值为1，根据SPS_S1、SPS_S2_M1与SPS_S2_M2模型描述的软件行为、时序特性，经分析得出满足规范1)、2)与3)的执行路径最大长度为9，故设置len 的取值为9。在执行片段提取过程中，通过在目标软件中进行插桩，实时判断当前执行片段是否符合规范要求，及时启动、终止执行片段记录过程，并保存已提取的执行片段。 为对TBTDD方法的时序缺陷检测能力进行全面考察，在测试环境中，采用卫星信号仿真设备，设置BDS系统的各类星况，激活SPS软件的各项运行剖面。在此情况下，持续运行SPS软件，按照以上规范在S1、S2_M1与S2_M2等阶段分别提取执行片段，从而使提取的执行片段集满足4.1.1节中所述的ESIA模型覆盖准则要求，以保证检测工作的充分性。 5.2  实验结果与分析 本节采用ATES平台内置的TBTDD方法，利用预先提取的执行片段集，在SPS_S1、SPS_S2_M1与SPS_S2_M2 模型之上进行软件运行时序检测, 并从执行片段集、缺陷检测等方面将TBTDD方法与Andrés，Morales与Núñez等提出的基于时间不变 量 的 时 序 缺 陷检 测 算 法[11-12]  (Timed Invariant-Based Defect Detection, TIBDD)进行比较。 Andrés，Morales与Núñez等在时间有限状态机模型(Timed Finite State Machine, TFSM)基础上，定义了时间不变量（Time  Invariant），对特定事件/行为序列上的时序特性要求进行描述，并将其作为时序检测的准则。在时间不变量设计中，采用一组时间区间限制特定行为序列上各项任务的执行时间，其形式为“导言→结论”。在此基础上，Andrés，Morales等提出TIBDD检测算法，对软件运行时序进行检测。当执行片段包含的行为序列、时间信息满足一项不变量导言部分的要求时，若软件后续运行过程中的行为序列、时间信息满足不变量结论部分的要求，则运行时序满足设计要求。 TBTDD方法与TIBDD算法的主要区别如下： 1）时序特性的描述方式不同。在TBTDD方法中，采用ESIA模型描述被测软件的时序特性，作为时序检测的基础模型。而在TIBDD算法中，以时间不变量描述被测软件的时序特性，需针对每一项时序设计要求分别定义相应的时间变量。 2）运行时序的检测过程不同。TBTDD方法依据执行片段可接受性准则、以及时序特性可满足性准则，在被测软件ESIA模型之上，检验执行序列包含的时间信息是否满足时序设计要求，进而发现相应时序故障。TIBDD算法则依据预定义的时间不变量，检验执行片段是否满足其导言、结论部分描述的时序设计要求。 3）时序检测的故障类型不同。根据时间约束相关性分析、时序缺陷分析结果，TBTDD方法可发现违反独立时间约束、违反相关时间约束、违反计时起点要求、异常时序处理错误等典型时序故障。而在TIBDD算法研究中，未对时间约束相关性、以及软件运行中可能存在的时序故障进行系统分析，其时序检测主要集中于对违反独立时间约束情况的检测。 4）时序检测的覆盖范围不同。TBTDD方法是一种通用检测方法，其检测范围覆盖被测软件ESIA模型所包含的全部时序设计信息，能否发现特定时序故障取决于提取的执行片段能否覆盖相应执行路径。TIBDD算法则多针对特定时序设计要求开展检测，能否发现某项时序故障不仅取决于执行片段的提取，还取决于时间不变量定义的内容。 由于TBTDD方法与TIBDD算法的工作目标不完全相同，故在实验过程中，仅对相关方面的实验论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  17 结果进行比较。 5.2.1  执行片段集 在实验过程中，在SPS软件运行的S1、S2阶段提取一系列执行片段。随后，在提取的执行片段集之上，通过聚类分析，合并同类执行片段，删除重复执行片段，共确定S1阶段执行片段3条，如表1所示；S2_M1阶段执行片段15条，如表2所示；S2_M2阶段执行片段15条。其中，S2_M2阶段执行片段集与S2_M1阶段类似。 表1 S1阶段执行片段集 序号  执行片段包含的行为序列  类型 1  Rcv_M1Inf? /CapP_M1? /Ret_Inf!  正常 2  Rcv_M1Inf? /CapP_M1_E? /Ret_ExcInf!  异常 3  Cap_C? /CapP_M2? /Ret_ExcInf!  正常  表2 S2_M1阶段执行片段集 序号  执行片段包含的行为序列  类型 1  CapP_M1? /Exe_Pos; /Ret_PosInf!  正常 2  CapP_M1? /Exe_Pos_E; /Ret_ExcInf! /CapP_M2? /Exe_Pos; /Ret_PosInf! 异常 3  CapP_M1? /Exe_Pos_E; /Ret_ExcInf! /CapP_M2? /Exe_Pos_E; /Ret_ExcInf! /Cap_C? /Exe_Pos; /Ret_PosInf! 异常 4  CapP_M1? /Exe_Pos_E; /Ret_ExcInf! /CapP_M2? /Exe_Pos_E; /Ret_ExcInf! /Cap_C? /Exe_Pos_E; /Ret_ExcInf! 异常 5  CapP_M1? /Exe_Pos_E; /Ret_ExcInf! /CapP_M2? /Exe_Pos_E; /Ret_ExcInf! /Cap_C_E? /Ret_ExcInf! 异常 6  CapP_M1? /Exe_Pos_E; /Ret_ExcInf! /CapP_M2_E? /Ret_ExcInf! /Cap_C? /Exe_Pos; /Ret_PosInf! 异常 7  CapP_M1? /Exe_Pos_E; /Ret_ExcInf! /CapP_M2_E? /Ret_ExcInf! /Cap_C? /Exe_Pos_E; /Ret_ExcInf! 异常 8  CapP_M1? /Exe_Pos_E; /Ret_ExcInf! /CapP_M2_E? /Ret_ExcInf! /Cap_C_E? /Ret_ExcInf! 异常 9  CapP_M1_E? /Ret_ExcInf! /CapP_M2? /Exe_Pos; /Ret_PosInf! 异常 10  CapP_M1_E? /Ret_ExcInf! /CapP_M2? /Exe_Pos_E;  异常 /Ret_ExcInf! /Cap_C? /Exe_Pos; /Ret_PosInf! 11  CapP_M1_E? /Ret_ExcInf! /CapP_M2? /Exe_Pos_E; /Ret_ExcInf! /Cap_C? /Exe_Pos_E; /Ret_ExcInf! 异常 12  CapP_M1_E? /Ret_ExcInf! /CapP_M2? /Exe_Pos_E; /Ret_ExcInf! /Cap_C_E? /Ret_ExcInf! 异常 13  CapP_M1_E? /Ret_ExcInf! /CapP_M2_E? /Ret_ExcInf! /Cap_C? /Exe_Pos; /Ret_PosInf! 异常 14  CapP_M1_E? /Ret_ExcInf! /CapP_M2_E? /Ret_ExcInf! /Cap_C? /Exe_Pos_E; /Ret_ExcInf! 异常 15  CapP_M1_E? /Ret_ExcInf! /CapP_M2_E? /Ret_ExcInf! /Cap_C_E? /Ret_ExcInf! 异常  以上执行片段集既包含正常时序片段，也包含异常时序片段，可利用其对目标软件各类运行时序、以及异常时序处理方式进行检测。在后续实验过程中，采用以上执行片段集，以SPS_S1、SPS_S2_M1与SPS_S2_M2模型为基础，开展执行片段匹配、相关时间约束分析、时序缺陷检测等工作，以验证TBTDD方法的有效性。 5.2.2  缺陷检测 在实验中，通过在被测软件中植入一系列时序缺陷，对TBTDD方法的时序缺陷检测能力进行验证。植入的时序缺陷包括违反独立时间约束、异常时序处理错误、违反相关时间约束、违反计时起点要求等故障类型，如表3所示。针对每种故障类型，分别植入了多项时序缺陷，检验TBTDD方法能否正确检测相应时序异常。此外，针对执行片段匹配过程，植入行为错配、行为错序等功能性故障，检验TBTDD方法能否检测相应功能异常。 以上植入的各类时序缺陷分布在SPS软件运行的S1、S2_M1、S2_M2等阶段内，针对各类独立、相关时间约束，覆盖各阶段的正常时序、以及异常时序处理分支。在缺陷植入时，通过设置特定行为的执行时间，使其违反相应独立、相关时间约束；或针对特定任务的计时区间，设置错误的计时起点，使任务执行时间的记录出现偏差，由此造成软件运行时序异常。表3 时序缺陷检测能力 缺陷类型  缺陷描述  TBTDD检测能力    TIBDD检测能力 行为错配  在S1阶段，提取执行片段Rcv_M1Inf? /CapP_M2? /Ret_Inf!  ，行为CapP_M2错配；  发现  发现 行为错序 在S2_M1阶段，提取执行片段CapP_M1? / Ret_ExcInf! /Exe_Pos_E; / CapP_M2? /Exe_Pos; /Ret_PosInf!，行为序列Ret_ExcInf! /Exe_Pos_E; 错序； 发现  发现 违反独立  在S1阶段，CapP_M1?  的执行时间低于D_Cstr(τ1)的下限；  发现  发现 18  计算机学报  2016年 时间约束 在S1阶段，CapP_M1?  的执行时间高于D_Cstr(τ1)的上限；  发现  发现 在S2_M1阶段，CapP_M1?  的执行时间低于D_Cstr(τ1)的下限, CapP_M1?执行  发现  发现 在S2_M1阶段，CapP_M1?  的执行时间高于D_Cstr(τ1)的上限；  发现  发现 在S2_M1阶段，CapP_M2?  的执行时间低于D_Cstr(τ3)的下限；  发现  发现 在S2_M1阶段，CapP_M2?  的执行时间高于D_Cstr(τ3)的上限；  发现  发现 在S2_M2阶段，CapC?  的执行时间低于D_Cstr(τ3)的下限；  发现  发现 在S2_M2阶段，CapC?  的执行时间高于D_Cstr(τ3)的上限；  发现  发现 在S2_M2阶段，Exe_Pos;  的执行时间低于D_Cstr(τ2)的下限；  发现  发现 在S2_M2阶段，Exe_Pos;  的执行时间高于D_Cstr(τ2)的下限；  发现  发现 违反相关时间约束 在S2_M1阶段，CapP_M1?  的执行时间满足D_Cstr(τ1)，Exe_Pos;  的执行时间满足D_Cstr(τ2)，同时二者违反C_Dep(τ1, τ2) ； 发现  未发现 在S2_M1阶段，CapP_M2?  的执行时间满足D_Cstr(τ3)，Exe_Pos;  的执行时间满足D_Cstr(τ2)，同时二者违反C_Dep(τ3, τ2) ； 发现  未发现 在S2_M1 阶段，CapC?  的执行时间满足D_Cstr(τ3)，Exe_Pos;  的执行时间满足D_Cstr(τ2)，同时二者违反C_Dep(τ3, τ2) ； 发现  未发现 在S2_M2阶段，CapP_M2?  的执行时间满足D_Cstr(τ3)，Exe_Pos;  的执行时间满足D_Cstr(τ2)，同时二者违反C_Dep(τ3, τ2) ； 发现  未发现 在S2_M2阶段，CapP_M1?  的执行时间满足D_Cstr(τ1)，Exe_Pos;  的执行时间满足D_Cstr(τ2)，同时二者违反C_Dep(τ1, τ2) ； 发现  未发现 在S2_M2 阶段，CapC?  的执行时间满足D_Cstr(τ3)，Exe_Pos;  的执行时间满足D_Cstr(τ2)，同时二者违反C_Dep(τ3, τ2) ； 发现  未发现 违反计时起点要求 在S1阶段，在Rcv_M1Inf?  执行结束时，τ1未置零；  发现  未发现 在S2_M1阶段，在Ret_PosInf!执行结束时，τ1与τ2未置零；    发现  未发现 在S2_M1阶段，在Ret_ExcInf!执行结束时，τ1与τ2未置零；  发现  未发现 在S2_M2阶段，在Ret_PosInf!执行结束时，τ3与τ2未置零；    发现  未发现 在S2_M2阶段，在Ret_ExcInf!执行结束时，τ3与τ2未置零；  发现  未发现 异常时序处理错误 在S2_M1阶段，CapP_M1?  的执行时间满足D_Cstr(τ1)，定位解算时间违反D_Cstr(τ2)，时序异常处理未被激活，Exe_Pos_E;未执行； 发现  发现 在S2_M1阶段，M1模式下的P码接收时间违反D_Cstr(τ1)，时序异常处理未被激活，CapP_M1_E;未执行； 发现  发现 在S2_M2阶段，CapP_M2?  的执行时间满足D_Cstr(τ3)，定位解算时间违反D_Cstr(τ2)，时序异常处理未被激活，Exe_Pos_E;未执行； 发现  发现 在S2_M2阶段，M2模式下的P码接收时间违反D_Cstr(τ3)，时序异常处理未被激活，CapP_M2_E;未执行； 发现  发现 在S2_M2阶段，CapC?  的执行时间满足D_Cstr(τ3)，定位解算时间违反D_Cstr(τ2)，时序异常处理未被激活，Exe_Pos_E;未执行； 发现  发现 S2_M2阶段，C模式下的C码接收时间违反D_Cstr(τ3)，时序异常处理未被激活，CapC_E;未执行； 发现  发现  实验结果显示，TBTDD 方法可正确发现以上29 项时序缺陷，表现出良好的缺陷检测能力。TIBDD方法可发现18项植入的时序缺陷，未发现违反相关时间约束、以及违反计时起点要求的时序异常。 TBTDD方法的时序缺陷检测能力主要受以下方面因素影响： 1）时间需求的描述。完整、精确的被测软件ESIA模型是时序缺陷检测的基础。EISA模型应完整、精确描述被测软件的时序特性，以支持对时序设计要求的正确分析与理解。 2）时间约束相关性分析。在时序检测中，不仅需检验各项任务的执行时间是否满足相应时间约束，还需检验任务的执行时间是否满足与其间接相关的时间约束。 3）执行片段的提取。提取的执行片段集合应满足ESIA模型覆盖准则要求，以保证时序特性检测的充分性。 4）执行序列的匹配与检测。时序检测准则、执行片段匹配算法、时序缺陷检测算法的精确性与执行效率均将直接影响TBTDD方法的时序缺陷检测能力。 TIBDD算法的时序缺陷检测能力主要受以下方面因素影响： 论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  19 1）时间不变量的定义。时间不变量定义的充分性、正确性将直接影响TIBDD方法的缺陷检测能力。在时序检测中，需要预估可能出现的时序异常，设计相应时间不变量。不充分的时序缺陷分析可能造成时间不变量缺失，使TIBDD方法无法发现相应时序异常。此外，若时间不变量的定义不符合规定格式、或不满足软件设计要求，则可能造成时序故障的检测、定位不准确。 2）TIBDD算法的时序缺陷检测能力同样受执行片段提取、算法的精确性与执行效率等方面因素的影响。 由以上分析可见，时间需求的描述、时间约束相关性分析等因素是造成TBTDD方法与TIBDD算法缺陷检测能力差异的主要原因。在TIBDD算法研究中，未对时间约束相关性、以及软件运行中可能存在的时序故障进行系统分析，其时间变量的定义未考虑违反相关时间约束、以及违反计时起点要求造成的时序异常，因而难以发现相应类型的时序故障。由此，理论上TBTDD方法具有比TIBDD算法更强的时序缺陷检测能力，其可检测的时序异常包含TIBDD方法能够检测的时序异常。若对时间不变量的定义、描述方式进行扩展，补充考虑时间约束相关性、以及计时区间设置等因素，则可进一步增强其发现相应时序故障的能力。 5.2.3   执行效率分析 TIBDD算法的执行需要预先定义一系列时间不变量，增加了额外的形式化工作；在对一组关联任务、或在复杂运行场景下进行检测时，时间不变量的形式将更复杂。针对不同任务剖面制定的时间不变量可能包含相同的独立时间约束，将造成时间约束的重复定义；当时序设计要求变更时，需对全部受影响的时间不变量进行调整，回归测试工作量大。此外，在时序检测过程中，TIBDD方法需要将每条执行片段与所有时间不变量的引语部分进行逐次匹配，当执行片段集合、时间不变量集合的规模不断增长、或不变量导言部分较长时，算法执行效率将受到显著影响。 TBTDD方法则直接利用ESIA模型描述的时间需求作为检测度量，无需定义时间不变量，避免了额外的形式化工作。通用的执行片段匹配与检测准则、以及完整的被测软件ESIA模型适用于各类运行场景下的时序特性检测，具有良好的适用性。若时序设计要求发生变更，仅需更新ESIA模型相关部分描述，支持便捷的回归测试。 5.2.4  局限性分析 在时序检测工作中，对领域知识的获取与理解、对时间需求的抽象与建模等更多依赖于测试人员的技术能力与工程经验，因此，ESIA模型构建可能存在完整性、准确性等问题，TBTDD方法可能无法检测到特定时序缺陷。在后续研究工作中，将进一步从设计与开发层面，研究利用ESIA模型对嵌入式软件时序特性进行完整、准确建模的方法。 1. 对时间约束间复杂依赖关系的处理 通常情况下，嵌入式软件中的时间约束相关关系主要存在于二项时间约束之间。当多项时间约束间存在多重相关关系时，不同时间变量之间的取值依赖关系将更加复杂。以上情况将导致时序缺陷检测过程更为复杂，缺陷的识别与定位也将更加困难。在后续研究工作中，针对时间约束间多重相关的情况，研究不同时间变量取值间复杂依赖关系的提取、描述与化简方法，考虑制定相关关系可满足性的一般准则，降低其检测复杂度，以期在较小的代价下对违反相关关系的异常时序进行充分测试。 2. 与行为特性相结合的混合特性检测 嵌入式软件执行路径由外部事件序列、触发事件产生时间、行为执行时间与变量、参数取值共同确定。在TBTDD方法中，仅对特定执行片段上的时序特性进行检测，而在执行片段之上，还存在一系列行为参数、内部变量等，其取值同样将影响软件运行状态与结果。此外，任务执行时间与变量、参数取值之间可能存在特定相互作用，参数的规模、取值等因素均可能影响软件运行时序。当前，对行为特性与时序特性的分离检测无法适应以上混合特性检测的要求。在后续工作中，考虑将嵌入式软件行为特性检测与时序特性检测相结合，研究建立通用的混合特性检测方法。 6  相关工作 在形式化测试方法研究中，基于执行序列的检测技术广泛应用于各类网络通信协议的测试工作。近年来，时序特性检测、基于状态机的行为特性检测等领域的研究工作取得了一系列成果，提出了各种不同的检测方法。 6.1  时序特性检测 学术界针对基于执行序列的时序特性检测技术开展了一系列研究。作为软件测试、形式化验证技术的有益补充，运行时序检测可在系统的设计、20  计算机学报  2016年 开发、确认、交付与维护等各个阶段实施，持续收集各类正常、异常时序信息，为系统时序特性设计方案的改进提供支持。运行时序检测技术兼顾软件测试与形式化验证的优点，利用真实的执行序列作为检测输入，利用形式化的功能、时间需求作为自动检测的依据，既可探查软件测试难以覆盖的特殊场景、特殊缺陷，也可避免模型检测带来的状态空间爆炸等问题。在系统交付之后，运行时序检测更成为状态监控、异常处理、以及维护保障的有效手段。 基于执行序列的时序特性检测技术主要可分为两类：一是基于时间模型的检测；二是基于时间规则的检测。在基于时间模型的检测中，采用包含时间信息的行为模型对被测软件时序特性进行完整描述，进而在被测软件模型之上通过执行序列匹配、时间信息检测等过程实施时序特性检测，例如本文提出的TBTDD方法等。在基于时间规则的检测中，采用时序逻辑对特定任务、运行场景的时间需求进行具体描述，制定一组形式化的时间规则，软件在运行的任何时刻均应遵循以上规则，进而利用该规则对提取的执行序列进行匹配与检测，例如前述TIBDD检测算法等。 2009年，Trinh，Do与Truong等提出一种基于UML时序图的实时软件系统时间约束检测方法[13]。在检测过程中，利用面向方面的编程技术(Aspect  Oriented  Programming,  AOP)在源代码中织入监控及检测代码，在软件运行过程中，实时提取任务执行信息、检验任务执行是否满足相应时间约束，并指出潜在的违反时间约束的时序故障。 2015年，Chen，Kumar提出一种基于线性时间逻辑(Linear-Time Temporal Logic, LTL)的离散时间随机系统时序特性检测方法[14]。在该方法中，使用离散差分公式描述物理系统在离散时间点上的动态特性，并以LTL描述其时间需求。通过精化过程，将物理系统的形式化描述、及其时序特性的LTL描述转化为I/O 随机混合自动机(Input-Output Stochastic Hybrid Automaton, I/O-SHA)模型。由此，物理系统的时序故障检测问题转化为I/O-SHA模型之上的状态可达性分析问题，即，若特定故障状态可达，则系统在运行时可能产生相应故障。该方法利用随机过滤方程(Stochastic Filtering Equation)估算系统在运行时抵达特定故障状态的概率，从而对故障发生的可能性进行评估。 以上方法采用的时序特性描述模型、故障检测方式与TBTDD方法均存在不同。在基于UML时序图的检测方法中，利用AOP技术在被测软件中织入监控及检测代码，将检测过程与软件运行过程交织在一起，而TBTDD方法则根据被测软件时间模型在后台实施检测过程。在基于线性时间逻辑(Linear-Time Temporal Logic, LTL)的检测方法中，通过可达性分析搜索故障状态，而TBTDD方法则根据预定义的检测准则判断软件运行是否产生时序故障。学术界对基于时间规则的时序特性检测技术进行了一系列研究，取得了更多的成果。 2008年至2009年间，Andrés，Merayo与Núñez等提出一种基于时间不变量的时序特性检测方法[15-16]。在时间有限状态机(Timed  Finite  State Machine, TFSM)形式化描述基础上，采用时间不变量描述目标软件的时间特性需求。一项时间不变量包括导言部分与结论部分，其中，导言部分表示为一个输入/输出行为序列，以及一系列约束行为执行的时间区间；结论部分表示为一个输入/输出行为对，以及相应时间区间。当提取的软件执行片段与导言中的输入/输出行为序列相匹配，且执行片段包含的时间信息满足相应时间区间的要求时，若软件在后续运行过程中表现出的行为与时序特性满足结论部分的要求，则软件运行时序满足设计要求，否则存在时序缺陷。在此基础上，其提出了运行日志的正确性检测算法，自动验证执行片段包含的时间信息是否满足各类时间不变量的要求，从而建立了完整的实时系统时序特性检测框架。 随后，Andrés，Merayo与Núñez等对以上时序特性检测方法进行扩展，以时间概率分布函数的形式，描述时间不变量中各项输入/输出行为的时间条件，从而对软件行为执行概率相对于运行时间区间的变化情况进行描述，并对运行日志检测算法进行适应性改进[17]。针对软件运行过程中在各个状态上的驻留时间，Merayo在时间不变量中增加一系列时间区间，以约束软件在特定状态上的驻留时间，进一步支持输入行为等待时间的验证[18]。此外，Andrés，Merayo等还讨论了从目标软件TFSM描述中自动抽取时间不变量的方法，以期提高以上方法的执行效率[19]。 Andrés，Merayo与Molinero等进一步针对目标软件执行片段，提出改变目标状态、改变行为输出等变异操作，通过对正常提取的执行片段执行变异操作，获得一组仿真执行片段，通过仿真片段集合检验时间不变量发现时序缺陷的能力[20]。 论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  21 2010年，Bessayah，Cavalli等提出一种基于精确时间逻辑(eXplicit  Clock  Temporal  Logic,  XCTL)的时间约束检测方法[21]。在此方法中，将各类复杂的系统时间需求描述为一系列XCTL公式，提出了时间需求一致性检测算法，并验证执行片段包含的时间信息是否满足XCTL公式描述的设计要求。 2012年，Wei，Huang与Cao等提出一种基于三值计算树逻辑(3-Valued  Computation  Tree Logic, CTL3)的普适计算时序特性检测方法[22]。在普适计算环境中，使用CTL3描述特定应用的时序特性：利用其三值语义(3-Valued Semantics)描述有限前驱行为序列下、后继行为序列的非决定性；利用分支时间(Branching Time)概念，描述普适计算环境异步性造成的预期行为的不确定性。在普适计算的运行时序检测中，以一组CTL3形式化描述为准则，检测特定应用的时序特性是否满足设计要求。 2014年，Zhao，Chai与Liu提出一种基于监测的列车控制系统时序特性检测方法[23]。针对LTL无法对时间约束进行定量描述的问题，作者提出一种度量区间时序逻辑(Metric  Interval Temporal Logic,  MITL)，用以对列车控制系统的时序特性进行定量描述。在此基础上，采用区间标记技术，提出一种增量式的在线检测算法，对运行过程中采集的执行片段进行持续检测，以判断列车控制系统的工作时序是否满足时间约束要求。 6.2  基于状态机的行为特性检测 1997年，Lee，Netravali与Sabnani等提出一种基于FSM 的行为特性检测算法，分为行为追踪(homing)与故障检测(fault detection)两个阶段[24]。在行为追踪阶段，针对提取的执行片段，在目标软件FSM模型之上搜索与其相匹配的执行路径，直到确定唯一的当前状态为止，转入下一阶段执行；在故障检测阶段，针对软件后续运行过程，持续检测当前行为的源状态是否为当前状态。在算法执行过程中，若当前行为的源状态不满足预期，则软件实现存在缺陷。2007年，Ural，Xu与Zhang针对以上算法提出了三类改进算法，通过避免冗余检测，使用特定数据结构缓存中间结果等措施，进一步提高算法执行效率[25]。 2001年，Zhao，Yin与Wu实现了一个路由协议在线测试系统(OnLine Test System, OLTS)，支持分布式环境中多重实例的在线检测[26]。OLTS通过一系列模块仿真路由信息的交换与控制过程，并通过状态同步算法，识别软件运行当前状态；通过拓扑分析，检测网络拓扑与设计要求的一致性，以检测路由协议与配置缺陷。2002年，他们进一步讨论了路由协议实时检测所面临的一系列问题，如计算任务量大、需要开放多个系统接口、路由配置复杂、路由信息获取困难等，并提出了相应改进措施[27]。 2002年至2006年间，Lee，Chen与Hao等在事件驱动的EFSM基础上，综合考虑行为前置条件中包含的变量约束条件以及不同变量间的依赖关系，提出一种数据特性检测方法[28-29]。在行为追踪与故障检测过程中，利用路径上的各项变量约束条件，持续精化变量取值区间，并判断变量在相应执行路径之上是否存在合理取值，若不存在则存在缺陷。2003年，Chen，Wu与Chu同样在事件驱动的EFSM基础上，针对具有复杂相关关系的变量取值范围难以确定等问题，提出采用整数线性编程技术(Inter Liner Programming, ILP)进行变量约束条件一致性检测，持续精化变量取值区间，以支持数据特性检测[30]。 2007年，Benharref，Dssouli与Serhani等提出一种加速行为追踪过程的方法，以提高在线检测方法的执行效率[31]。在在线检测过程中，当观察到一个事件或行为时，在EFSM之上执行一步正向行为匹配；在等待下一事件或行为的间隙，在EFSM之上执行一步逆向行为追踪，以推导可能导致当前状态的执行路径；在以上正向/逆向相结合的检测过程中，构建执行树，加速行为追踪过程。 7  总结 时序测试是检验嵌入式软件时序特性是否满足设计要求、对各类异常时序能否进行正确处理的有效手段。本文提出一种基于执行序列的嵌入式软件时序缺陷检测方法TBTDD。在目标系统ESIA模型之上，制定了一组时序特性检测准则，通过收集目标软件执行片段集，依据匹配的ESIA执行路径上的各项独立、相关时间约束，对其包含的时间信息进行离线检测，从而发现软件实现中隐藏的时序缺陷。本文对不同时间约束间相关关系类型进行讨论，在时序检测过程中，针对时间约束间相互作用的情况，分类检测违反特定时间约束、违反相关时间约束、计时起点错误等时序缺陷。 实验结果表明，TBTDD方法可有效检测软件运行过程中的各类时序异常，避免了环境因素对时序测试工作的影响，与传统时序测试方法配合使用22  计算机学报  2016年 时，可对目标软件时序特性进行更充分的测试，提高了测试的有效性和充分性。在后续工作中，将对多项时间约束之间存在多重相关关系的情况进行研究，并对检测流程与算法进行进一步优化，研究运行时序异常的在线检测与故障定位方法。 致  谢  在此,  我们向对本文工作给予支持和建议的同行,  特别是实验室内各位老师和同学表示感谢. 参 考 文 献 [1]  Alur  R,  Dill  D  L.  A  theory  of  timed  automata.  Theoretical  computer  science,  1994,  126(2):183-235. [2]  Lutz  C,  Wolter  F,  Zakharyaschev  M.  Temporal description logics: A  Survey.  //Proceedings  of  the 15th  International  Symposium  on Temporal  Representation  and  Reasoning.  Montreal,  Canada,  2008:3-14. [3]  Yin  YF,  Liu  B,  Ni  HY.  A  survey  on  the  formal  testing  techniques  for  real-time  embedded  software.  //  Proceedings  of  the 2th  International  Conference  on  Information  Science  and  Engineering.  Hang  Zhou,  China,  2010:6426-6429. [4]  De  Alfaro  L,  Henzinger  T  A.  Interface  Automata.  //  Proceedings of  the 9th  Annual  Symposium  on  Foundations  of  Software  Engineering.  New  York,  USA,  2001:109-120. [5]  Wang  B,  Bai  XY,  Zhang  C,  He  F,  Song  XY.  Test  Case  Generation for  Embedded  Software Using Interface  Automata  and  Symbolic  Execution.  Chinese  Journal  of  Computers,  2015,  38(11):2125-2144.  王博,  白晓颖,  张超,  贺飞,  Song  XY.  基于接口自动机与符号执行的嵌入式软件测试用例生成.  计算机学报,  2015,  38(11):2125-2144. [6]  Dasarathy  B.  Timing  Constraints  of  Real-Time  Systems:  Constructs  for  Expressing  Them,  Methods  of  Validating  Them.  IEEE  Transactions  on  Software  Engineering,  1985, 11(1):80-86. [7] Lee  D,  Netravali  A  N,  Sabnani  K  K,  Sugla  B,  John  A.  Passive  testing  and  applications  to  network  management.  //  Proceedings  of  the IEEE  International  Conference  on  Network  Protocols.  Atlanta, USA,  1997:113-122. [8] Miller  R  E,  Arisha  K  A.  Fault  identification  in  networks  by  passive  testing.  //  Proceedings  of  the 34th  Annual  Simulation  Symposium.  Washington, USA,  2001:277-284. [9]  Miller,  R  E.  Passive  testing  of  networks  using  a  CFSM  specification.  //  Proceedings  of  the 17th International  Performance  Computing  and  Communications  Conference.  Phoenix/Tempe,  USA,  1998:111-116. [10] Alcalde  B,  Cavalli  A,  Chen  D,  Khuu  D,  Lee  D.  Network  protocol  system  passive  testing  for  fault  management:  A  backward  checking  approach.  //Formal  Techniques  for  Networked  and  Distributed  Systems–FORTE.  Berlin  Heidelberg:Springer,  2004:150-166. [11] Andrés  C,  Merayo  M  G,  Núñez  M.  Passive  testing  of  timed  systems.  //Automated  Technology  for  Verification  and  Analysis.  Berlin  Heidelberg:Springer,  2008:418-427. [12] Morales  G,  Maag  S,  Cavalli  A,  Mallouli  W,  De  Oca  E  M,  Wehbi  B.  Timed  extended  invariants  for  the  passive  testing  of  web  services.  //  Proceedings  of  the IEEE  International  Conference  on  Web  Services.  Miami,  USA,  2010:592-599. [13]  Trinh  T.  B,  Do  T.  A,  Truong  N.  T,  Nguyen  V.  H.  Checking  the  compliance  of  timing  constraints  in  software  applications.  //  Proceedings  of  the International  Conference  on  InKnowledge  and  Systems  Engineering.  Hanoi,  Vietnam,  2009:220-225. [14] Chen  J,  Kumar  R. Fault detection  of discrete-time stochastic  systems subject  to temporal logic correctness requirements.  IEEE  Transactions  on  Automation  Science  and  Engineering,  2015, 12(4):1369-1379. [15] Andrés  C,  Merayo  M  G,  Núñez  M.  Formal  correctness  of  a  passive  testing  approach  for  timed  systems.  //  Proceedings  of  the 2th IEEE  International  Conference  on  Software  Testing,  Verification  and  Validation  Workshops.  Denver,  USA  2009:67-76. [16] Andrés  C,  Merayo  M  G,  Núñez  M.  Applying  formal  passive  testing  to  study  temporal  properties  of  the  stream  control  transmission  protocol.  //  Proceedings  of  the 7th  IEEE  International  Conference  on  Software  Engineering  and  Formal  Methods.  Pisa,  Italy,  2009:73-82. [17] Andrés  C,  Merayo  M  G,  Nuez  M.  Passive  testing  of  stochastic  timed  systems.  //  Proceedings  of  the 2th  IEEE International  Conference  on  Software  Testing  Verification  and  Validation.  Denver,  USA,  2009:71-80. [18] Merayo,  M G.  Passive  testing  of  timed  systems  with  timeouts.  //  Proceedings  of  the 12th  IEEE  International  Conference  on  Quality Software. Xi’an, China,  2012:69-78. [19] Andrés  C,  Merayo  M  G,  Nuez  M.  Supporting  the  extraction  of  timed  properties  for  passive  testing by  using  probabilistic  user  models.  //  Proceedings  of  the 9th IEEE  International  Conference  on  Quality  Software. Jeju,  Korea,  2009:145-154. [20] Andrés  C,  Merayo  M  G,  Molinero  C.  Advantages  of  mutation  in  passive  testing:  An  empirical  study. //  Proceedings  of  the 2nd  IEEE International  Conference  on  Software  Testing,  Verification  and  Validation  Workshops.  Denver,  USA  2009:230-239. [21] Bessayah  F,  Cavalli  A.  A  Formal  Passive  Testing  Approach  for 论文在线出版号  No.170  王博等：基于执行序列的嵌入式软件时序异常检测  23 Checking  Real  Time  Constraints. //  Proceedings  of  the 7th  IEEE International  Conference  on  the Quality  of  Information  and  Communications  Technology.  Porto,  Portugal,  2010:274-279. [22]  Wei  H,  Huang  Y,  Cao  J,  Ma  X,  Lu  J.  Formal  specification  and runtime  detection  of  temporal  properties  for  asynchronous  context.  //  Proceedings  of  the 2012  IEEE  International  Conference  on  Pervasive  Computing  and  Communications.  Lugano,  Switzerland,  2012:30-38. [23] Zhao  L,  Chai  M,  Liu  Y.  Monitor-based  temporal  properties  checking  of  train  control  systems  with  quantitative  constraints.  //  Proceedings  of  the 17th  International  IEEE  Conference  on  Intelligent  Transportation  Systems.  Qingdao,  China,  2014:2846-2851. [24] Lee  D,  Netravali  A  N,  Sabnani  K  K,  Sugla  B,  John  A.  Passive testing  and  applications  to  network  management.  //  Proceedings  of  the IEEE  International  Conference  on  Network  Protocols.  Atlanta,  USA,  1997:113-122. [25] Ural  H,  Xu  Z,  Zhang  F.  An  improved  approach  to  passive  testing  of  FSM-based  systems.  //  Proceedings  of  the 2nd  IEEE  International  Workshop  on  Automation  of  Software  Test.  Minneapolis,  USA, 2007:6. [26] Zhao  YX,  Yin  X,  Wu  JP.  Online  test  system,  an  application  of  passive  testing  in  routing  protocols  test.  //  Proceedings  of  the IEEE  9th  International  Conference  on  Networks.  Washington,  DC,  USA,  2001:190-195. [27] Wu  JP,  Zhao  YX,  Yin  X.  From  active  to  passive:  Progress  in  testing  of  internet  routing  protocols.  //  Proceedings  of  the 22th International  Conference  on  Formal  Techniques  for  Networked  and  Distributed  Systems.  Houston,  USA,  2002:101-116. [28] Lee  D,  Chen  D,  Hao  R,  Miller  R  E,  Wu  JP,  Yin  X.  A  formal  approach  for  passive  testing  of  protocol  data  portions.  //  Proceedings  of  the 10th  IEEE  International  Conference  on  Network  Protocols.  Paris,  France,  2002:122-131. [29] Lee  D,  Chen  D,  Hao  R,  Miller  R  E,  Wu  JP,  Yin  X.  Network  protocol  system  monitoring:  a  formal  approach  with  passive  testing.    IEEE/ACM  Transactions  on  Networking,  2006,14(2):424-437. [30] Chen  D,  Wu  J,  Chu  T  I.  An  enhanced  passive  testing  tool  for  network  protocols.  //  Proceedings  of  the International  Conference  on  Computer  Networks  and  Mobile  Computing.  Shanghai,  China,  2003:513-516. [31] Benharref  A,  Dssouli  R,  Serhani  M  A,  En-Nouaary  A,  Glitho  R.  New  approach  for  EFSM-based  passive  testing  of  web  services.  //Testing  of  Software  and  Communicating  Systems.  Berlin  Heidelberg:Springer,  2007:13-27.WANG Bo, born in 1979, Ph. D. candidate. His main research interests include software testing and embedded system.        BAI Xiao-Ying, born in 1973, Ph. D., associate professor. Her research  interests  include  software  testing  and  service computing. CHEN  Wen-guang,  born  in  1972,  Ph.  D.,  professor.  Her research interests include parallel and distributed computing. Xiaoyu  SONG,  born  in  1963,  Ph.  D.,  professor.  Her  research interests  include  formal  methods  and embedded  computing system.Background Timing  constraints  are  critical  to  real-time  embedded software. Mission-critical  and  safety-critical  systems,  such  as avionics electronics  and  high-speed  railway  operation,  usually have hard  timing  requirements.  Temporal  defects  may  cause runtime  abnormities,  even  disasters.  However,  it  is  hard  to verify  and  validate  system  temporal  correctness  when  there exist  multiple  timing  constraints  with  complex inter-dependencies. Temporal defect detection using timed execution trace has been applied in verification of timing characterisics. It  aims to reduce the  impact  of  test  environment  and  test  engineer  while enhance effectiveness and  maintainability of temporal testing through  formal method. The  paper  proposes  a temporal  defect detecting method using execution trace of embedded software. A model called Extended Semantic Interface Automata (ESIA) with  temporal  semantics  is designed  to  capture  timing characteristics  including time  variable, timing  constraint,  and reset action. It assumes that with sufficient domain knowledge, the  model  can  provide  a  formal  description  of  the  expected timing  characeristics  that  the  software  exposes.  Execution traces  with  time  information  are  extracted  in  running environment  of target  system, and correlations between timing  24  计算机学报  2016年 constraints  on  execution  trace  are  analyzed.  Both  normal temporal and temporal exception are checked based on analysis of constraints along test paths. Experiments  are  exercised  on  a  satellite  positioning system  using  BeiDou  Navigation  Satellite  System  (BDS) signals.  The execution  traces  are extracted  on  an  in-house developed environment with target  software. The ESIA model is  built  based  on timing  requirements  of  target  sotware.  The detecting effectiveness and efficiency are compared with other formal testing methods such as temporal defect detecting using timed invariants. This research  is  supported  by National Natural Science Foundation  of  China  (91218302,  61472197),  and  Beijing Natural Science Foundation (4132062).