TinyOS论文12：Inter-Context Control-flow and Data-FlowText

nesC语言程序上下文间、控制流和数据流的测试充分性标准。

Abstract

这里的context指的是：中断触发的一系列操作（中断处理程序）；

程序执行时高度的inter-context交错很容易导致程序出错。例如交错执行的程序中共享变量的改变；

论文对可能交错执行的context建模成inter-context流图，基于这些图形，提出了两种测试充分性标准：inter-context数据流和inter-context控制流

1、Introduction

通过相互协作的事件处理程序实现NesC应用，而通过高度的基于中断的并发来实现事件处理程序的协作。

NesC程序开发人员需要处理大量的中断，涉及的问题有：数据竞争，interface-contract的违反和内存安全错误等。

现有的并发程序测试技术采用的方法是：通过识别同步原语来识别并发程序间的交错执行，但是实际中这种交错执行很大，很难实现充分的测试覆盖。

一个NesC程序一般包括两中子程序(subroutine)：任务 + 中断处理程序

nesC程序的执行机制：

1、中断处理程序能够抢占其它中断处理程序和任务；

2、一个中断处理程序会一直执行到结束除非有其它中断处理程序发生了抢占；

3、任务的执行是FIFO。

这三种调度机制使得NesC程序的并发机制处理起来比任意的线程并发机制简单很多。

论文提出了针对NesC程序测试的框架：

1、首先，对要执行的task建模成task图；

2、然后基于task图提出了Inter-context流图(ICFGs)，ICFGs不仅捕获subroutine程序间的转换，并且捕获交错执行subroutine程序间的数据交互。

3、再在ICFGs的基础上提出了控制流和数据流测试充分性标准来评估测试用例对subroutines程序的覆盖率。

论文贡献：

1、针对NesC程序建模的ICFG

2、提出了两种对NesC程序测试用例的测试充分性标准

3、两种标准的对比：所有分支标准 + 所有使用标准；

2、fundamentals

nesC语言基础

1、中断转换成相应的事件，传给相应的事件处理程序来处理

2、异步事件处理程序(AEH)：异步 + 执行时间短 + 将耗时操作交给task + 可抢占除非atomic

3、A motivation example

Oscilloscpoe(TinyOS1.x)执行过程

1、OM声明的两个共享变量：packetReadingNumber 和msg + 四个任务task1234 + 三个事件处理程序 + PhotoSensor.dataReady、SendMsg.sendDone、TempSensor.dataReady

2、OM的实现功能：采集光和温度传感数据，将采样数据保存在buffer中，并且发送到基站；更具体一点的执行步骤是：

①、获得传感数据后，调用PhotoSensor.dataReady数据存储在共享变量msg.data缓存中；

②、缓存满时，post task2处理缓存数据；由于处理缓存的计算量很大，放置其它task饿死的现象，对task2处理缓存任务进行分解处理；

③、task2最后将对缓存的处理结果发送给基站。

OM程序存在的bug：在task2处理缓存的时候，dataReady接收到了新的数据，覆盖了原有的数据，导致发送不正确的数据包给基站

论文的观点：设计的测试用例要求满足某种特定的抢占场景，这里即在task2处理缓存数据的时候，发生新的中断触发PhotoSensor.dataReady获取到了新的数据。测试用例如果会覆盖抢占和恢复(抢占——任务)更有利于发现bug

4、representation

介绍对NesC程序建模的ICFG

preliminaries

block：未发生抢占的语句执行：entry块 + exit块(return语句) + 原子块 + 非院子块。FG与CFG不同之处在于，FG的节点表示块而不是语句

三元组(v,d,u)：(变量、定义、使用) + definition-clear：v没有被重新定义

使用任务提交树来描述任务提交语句序列的关系 + 使用任务图来描述任务序列执行的关系 + 任务抢占被直接定义成ICFG

定义1：任务提交树(TPT)：中断程序u是一个有向树的2元祖G(TPT )=(N,E)，N是提交语句，边E满足一下两个条件：Ni支配Nj + 如果Nk支配Ni,则也支配Nk。

Ni支配Nj ：每一个达到Nj节点的有向路径都包含有Ni + 支配树：根节点是entry节点，每一个节点只支配他的后代节点，支配树的构造是基于CFG(通过移除非post语句)

定义2：任务图(TG )：节点表示任务、边表示任务间的执行顺序，根据TPT得出TG。TG只表示任务间的交互

Inter-context Flow Graph



描述中断处理程序的抢占和恢复，ICFG是基于TG的，ICFG主要是联系单独中断处理程序流图，通过制定的中断处理和延迟执行的任务。

闲置节点：没有明显要执行的中断处理程序(即等待即将到来的中断)

ICFG四种类型的控制流边

1、幻影边：连接不同Context间的中断处理程序和任务：例如进入一个新的中断处理程序节点(没有中断到又中断 + 一个中断完成进入下一个中断)

2、抢占边：对中断发生时的抢占建模；(n9-n6)

3、恢复边：抢占的中断处理程序执行完成（n6-n9）；

4、任务顺序边：提交任务的执行顺序进行建模；(两种情况：n6-n13 + n13 - n6)

ICFGs图定义：六元组,<中断处理程序对应的FGs、闲置节点、四种类型的变>

讲解一下ICFGs图的执行过程。

测试充分性标准

提出了测试充分性标准来测量nesC程序测试用例的质量

标准1：测试用例T满足all-inter-context-edges，对于每一条边，至少有一个测试用例执行时会覆盖；

Data-Flow 充分性标准：用于选择合适的测试用例来检测非法的数据使用

1、算法实现了获得共享变量的定义-使用关系。

标准2：测试用例T满足all-inter-context-uses，对于每一个定义-使用关系，至少有一个测试用例执行时会覆盖

5、实验

实验目的：满足这两种充分性标准的测试用例集能够有效监测NesC程序的bug

experimental setup

被测程序Sentri

结构健康监测程序：用于评估结构的状态和监测结构的改变如何影响结构的性能。

植入错误

往被测程序Sentri中植入错误 + 创建故障类(模板) + 从故障类中提取64个bug + 每一个错误实例包含16中错误类 + 测试池 + 排除7个失败率概予0.1的错误版本和8个没有测试用例检测的错误版本 + 剩下的49个左右错误版本

模拟setup

1、Avrora + java + python + 测试输入：模拟配置、消息序列和中断调度

2、模拟配置：Avrora、mica2节点、ATMegal单片机，模拟时间在1ms——20000ms之间，且模拟时间决定发送的消息数量和生成的中断数量

3、消息序列：驱动向测试节点发送消息的间隔1ms——1000ms之间随机；

4、中断调度：抽象成一个二元组(vector time)表示(中断号、合适触发)

(Avrora)收集的模拟结果包括：LED转换的状态 + 从radio发送出去的消息 + 从UART发送出去的消息 + I/O寄存器的改变

Experimental Design