外文翻译译文-TinyOS的接口协议

0附件1：外文资料翻译译文TinyOS的接口协议作者：1.WillArcher.计算犹他大学，E-mial地址：。2.PhilipLevis.斯坦福大学计算机系，E-mial地址：。3.JohnRegehr.计算犹他大学，E-mial地址：。摘要TinyOS应用程序是由一些通过接口相互联系的组件构成的。因为组件使小块代码重用，使其内核程序和内存的需求非常小，很适合无线传感器网络的应用。然而,其它的重要的好处部件快速开发应用程序的重用能力基本上仍未通过黑盒测试，因为在很多情况下接口有隐含的使用限制，即可令人沮丧的程序错误的来源。开发商通常是被迫阅读组件的源代码，部分人放弃把组件放在第一位使用的目的。我们的研究有助于解决这些问题，明确允许开发者指定构件接口和执行协议。由于常见接口的广泛的重用，执行少数接口频繁重用的协议，允许我们广泛检查大量的应用程序。我们发现了一些微妙的和以前不为人知的应用程序的错误，这些错误已经在通常的使用中存在多年了。分类和学科描述符D.2.4软件工程：软件/程序验证协议规划；D.2.5软件工程：测试和调试测试工具。一般条款设计、可靠性、验证关键词确认协议设计TinyOS传感器网络自动化测试1.介绍TinyOS已经是一个成功的基础的中断驱动应用程序。其组件的模式是减少应用代码大小，只用连接在只需要的功能，和提高应用程序开发构件的复用速度。不幸的是，创造可靠的TinyOS应用程序，建造在现有组件，特别是别人写的那些，是非常困难的。一个主要的挑战是，正确的使用TinyOS接口从未1经过精心的规定。不能给开发者的想要的自由。用户服务层用户服务层协议图1一个接口协议执行正确使用nesC介入的界面操作界面之间的用户和供应商可复用组件的开发人员被迫假定它们的接口会被滥用而需要谨慎编程，增加发展和资源的开销。同样，那些重用已有组件接口被迫承担即使正确使用，访问也可能失败得后果，错误检查和故障恢复策略对上层的发展是很必要的。上述的这些问题，已经被证明是和TinyOSl.x的接口设计中存在的一些相关的问题。这篇论文就是我们检查过得出的结论，我们相信这些问题也会出现在TinyOS2.0。为了进一步解决这些问题，我们开发了TinyOS接口协议。图1中所描述的接口协议是一个可检查的、可执行的，关键字概括说明(以前没有言明)正确使用一个接口的规则。为了检查不符合协议的组件，我们通过动态的端到端的协议检查程序转变，对现有TinyOS应用增加了检查，例如一个接口的滥用提高了错误。协议给开发者提供了很有价值的命题：协议对于一个给定的接口只定义一次，然后任何一个实例的接口可以重复使用它。同样的,多个应用程序的多次和随时的重用给了协议很大的潜力：TinyOSl.x核心接口一直稳定保持了好几年。在现有的TinyOS程序引入一个高效率的检测系统协议需要解决三个难题。第一个问题是定义协议。这就要求学习TinyOS代码库中预期的访问模式，其中许多是特殊的和一些以传统方式存在于源代码中的不同地方。为一个已经存在多年但没有协议的系统做一个协议是需要很大努力的。例如，我们一再发现，即使是我们相信很久的协议，因为应用程序的侵犯变得很脆弱。第二个问题是解决nesC特点和传统语言的观念。nesC的语言有几个高级功能,如函数的“输出端到多个访问者”访问能力，这是协议必须能支持的。第三个挑战是定义一2个协议语言可以处理前两个挑战，这是很容易理解的，而且不必考虑传感器网络节点重要资源的高度制约。图2没有接口协议故障进行隔离(左)，在复杂的TinyOS应用中是很困难的。协议(右)支持通过不断快速、高效的检测检查接口故障。我们的最终目标是使每个接口都有协议，包括底层的硬件抽象层。当任意的输入都有独立的测试时，就能让单元测试在一个模拟环境中进行。在模拟环境中进行单元测试将发现一些但并非所有的错误；而在充分运行应用中，实际节点也应该能够有效的实施协议。每包几百次传输可能是无误的，但并不是在每个广播的中断字节都可行。我们的研究主要有两个好处。在短期内,就像图2所示，作为可测试的协议，那些使开发人员更容易创造错误的可执行文件，和快速定位不正确的程序代码。从长远来看,我们预计它将可能使用正规的静态方法检查整体和单个不符合其接口协议的应用组件。检查独立的部件是非常艰巨的工作，因为它证明一种特殊的组件在任何可能的实例化中是正确的，而不仅仅是在其中一个。此外，我们希望组件的层面检查来是有用的，在一个假设确定推理方案5，可以归纳的证明一个完整的应用程序是正确的。2.TINYOS背景TinyOS7是一款基于组件的操作系统，其组件通过类型化协议相互作用。这个操作系统是用nesC4写的，一种支持组件的C的方言、接口、并发分析、网络类型。建立一个TinyOS应用程序需要将涉及的组件接口连接在一起。接3口是双向的，这种接口实际上是提供者组件和使用者组件间的一个多功能交互通道。一方面，接口的提供者实现了接口的一组功能函数，称为命令；另一方面，接口的使用者需要实现的一组功能函数，称为事件。例如，发送信息包是一个命令，而接受信息包是个事件。一般说来，一个接口支持一条狭长而完整的抽象的例如使用一个定时器，发信给一个非稳定性记录，或接收数据包。图3:发送信息的接口图4:定时器接口TinyOS不支持阻断。相反，缓慢的操作特别是那些涉及硬件潜在因素的是分相型的。举个例子，图3显示基本的信息包通信接口（SendMsg）。而不是等到操作（SendMsg.send）完成，接口命令就立即返回，允许应用程序继续处理。当操作都完成,接口表示完成的事件（SendMsg.sendDone)，在此情况下该用户可以回收包缓冲区。分相式语法具有许多优势，但这对于那些被迫明确地维持多重的组件技术的开发商而言也造成了困难。分相式操作是我们所发现的相当多的误用的接口来源。一个执行否则无法声明另一个组件：组件交互作用仅通过接口。这明确的分离可以让程序员容易改变已经被使用的实现。例如，一个组件名叫“AppM”使用”SendMsg”可直接连接到一个单极性的通信堆栈,一个多极性混4合堆栈，或一发送队列，而没有改变AppM的代码。能够轻易转换不同接口的实现方式要求实现是可互换的。不幸的是，目前，大多数接口并没有准确语义标准和驱动的模式。因为有一个很好的协议的实施范围，一个组件必须能承受广泛范围的行为。这导致冗余的代码，所以必须编程保护每个组件。3.设计协议制度这一节将描述我们的协议语言和开发者如何可以用它来指定一个接口的语义。3.1协议语言为了提供开发者以熟悉的环境，我们的协议是C语言一个指定版本。图4显示了TinyOS计时器接口和图5阐述了一个接口命令的协议。在这个例子里,只有命令返回SUCCESS，Timer.startO)指令执行一个状态转移。一个接口的协议包含“PRE”和“post”两部分。在后置条件和前提条件代码放置的地方。在图5中,安全检查放在前面是为了尽早地发现一个错误。协议根据规定检查接口调用，并且根据这些对顶层也检查数据。协议用一种特殊的R-VAL变量可以访问一个调用的返回值。如图5所示，返回值常被用来表示一个调用的成功或失败。协议代码可以描述状态变化。一个变量的独立拷贝是协议在一个应用程序中的实例化。特殊的变量ID是接口变量参数化的映射，应该是可实现的。它为让错误信息更有用提供便利。协议不被允许访问组件的不通过接口流动的内部信息。这会违反我们对协议接口的设计原则。一些接口协议,如在图5中,可以在检查接口的状态过程中表示出来。在其他情况下，接口本身是没有状态的，协议使数据结构在应用中有执行的先决条件和后置条件。这是SendMsg接口案例见图3。支持这种接口，我们允许协议来支持这些数据结构新领域以及访问这些领域。举个例子，图6显示了一个状态变量被添加到TinyOS数据结构缓冲区内。在这种情况下，当一个缓冲区被传送到SendMsg.send（）时,一个额外的send（）请求时不可行的，除非sendDone()事件被激活。因此，在完成第一个请求之前试图发送同一个缓冲区两次将是对一个协议的侵犯，但是使用不同的缓冲区则不会这样。5图5Timer.start（）命令的协议3.2协议的撰写首先，也是最重要的是，刚开始要编写接口所暗含的状态原理，除非这个过程做的很出色,否则把协议写正确是很难的，这要求我们有大量的时间在开发的部分。我们的工具的一个重要贡献是提供一组最晦涩、最常用的TinyOS接口协议。通过提供这些，我们能够比较彻底检查现有应用程序最小额外的编程。一旦一个状态机，封装该接口的行为已确立，可转换被翻译成可执行的协议。SendMsg接口（图3）的状态机制如图7示。图8显示了在我们的示例应用程序中的接口和我们正在检查的数量有多少。通过只运行一些有趣的接口检查，我们能够覆盖大约接口实例的总语句数的一半。对于本文中，我们着重已6经相当普及的接口，以适用于各种应用和有趣的足有可能含有价值的错误。尽管有大量的接口我们图6SendMsg.send()命令的协议图7：SendMsg接口的状态原理不包括，其中大部分都不是稳态，因此不需要协议，或者是针对个人申请的。3.3错误和警告我们开始认识到，违反协议的严重性有多种，我们通过了该协议的违规行为分为两大类。警告注明使用是在很低的级别，但据我们所知，并不是直接导致应用程序发生故障。例如，一个警告是一个应用程序初始化时生成一个已经7使计数器开始运行的计时器组件。更严重的就成了错误，这表明行为不可能是正确的，如同时通过一个单一的数据包缓冲区多次接收子系统。安全控制时间发送接收容器时钟灯数模数转换模数转换控制通道控制其他BlinkTask32003220003CntToLedsAndRfm1566722330023Surge258121222684323Surge-TinySec268141422684349SurgeReliable3710131222340361图8：每个接口被一些TinyOS的应用的次数4.检验协议我们创建了一个源到源转换工具，输入一组协议和C代码nesC的编译器产生，并输出一个新的C程序，运行时，动态检查接口的协议。我们的工具是基于CIL的12，一个分析器，类型检查，以及C的中间表示。4.1增加协议检查我们的工具，如图9所示，执行以下步骤。接口的命名。由于接口名称在nesC的编译器输出时会模糊，我们的工具需要在前面增加一些额外的信息来加强协议的检查。nesC的编译器选择性的去掉这个作为一种XML的路线信息。我们利用这个功能来映射C代码在发出的实际接口实例的函数名。构建调用图和应用从源代码布线。nesC的编译器使用明确定义的名称重整计划，允许我们直接从编译器的输出恢复组件接线信息。除了分离函数名的错位和了解给定应用程序接口定义，我们知道哪些函数实现一个给定的接口，它们属于哪个组件。我们还从应用程序代码建立整个程序调用图，我们在下面说明的支持最优化。增加协议检查代码。在TinyOS接口包含两个函数调用命令和事件，需要我们的工具进行不同的处理。我们通过开始部分的前置代码和所有返回前的后置代码处理命令。稽核事件，需要不同的方法使代码从低级别上移。因为可能在回调之前有逻辑性的必要，我们不能想当然地认为，状态在传递中出现问题是在接口函数的开始。出于这个原因，我们仪器之前和之后分别回调，在回调的返回值的R_VAL需要时堵塞。增加协议状态变量。协议状态变量有两种类型：每接触，每个数据结构。每个协议的变量是作为新的全局变量直接添加。8每个数据结构变量附加到现有的结构结尾。图9：在一个TinyOS的应用中，添加动态检查协议的基础结构4.2优化避免重复检查。我们发现，通常情况下，TinyOS接口的多种用途直接通过从一个组件到另一个不执行任何有用的计算要求。通常，这些调用没有引进上层，因为他们通过内联函数被删除。但是，如果我们使用协议处理所有接口的使用，开销将是巨大的。作为一个优化，我们避免在没经过任何额外的执行检查协议处理的情况下，一个组件从一个接口到另一个接口被调用。内联和清理。nesC的编译器尝试通过小的内联函数和函数调用点生成小的目标代码。我们发现，协议检查代码加入到nesC编译器的输出，通过使功能强大决定内联的决定无效，由40或以上的可能导致大型代码崩溃。在以前的工作中3,14，我们为C语言开发了一些内联函数和强壮的无效代码处理器。我们使用这些工具减少接口代码。在协议添加之后我们的内联函数用它的代码的大小来做出正确的决定。4.3处理协议的不规范行为9当协议被违反，我们有多种错误报告和采取纠正的措施。为了支持一个在Avrora17中更精确的周期的传感器网络模拟器的应用测试，我们以一个简单的类似printf函数的模拟器控制台提示警告和错误。当协议的应用程序是建立在真正的硬件上运行，我们使用三个小型的闪烁的LED以八进制的形式表示错误代码。此代码可以用单独的脱机工具变成一个源代码。我们还没有实现这一点，在布署无线传感器网络，违反协议应使用一个日志服务记录在网络中，和节点应该重新启动。5.结果本节总结了结果，以增加动态检查一些TinyOS1.x应用程序。5.1架空动态检查在图10显示了数据大小，代码大小和在图11中列出了接口动态检查协议百分比变化占空比。正如在第4节所述，我们用我们的内联函数和死代码消除函数，以避免不必要的资源膨胀。为了确保公平的比较，图10中的数字比较原始的应用程序，内联和清理（减少相对于默认的编译代码和数据的大小的百分之几）对于协议检查、内联和清理的错误应用程序。占空比的一小部分时间花在传感器网络应用该处理器运行使用Avrora17的计算。我们的应用上最重要的影响是，通过增加跟踪接口的状态变量来增加数据的大小。我们将字段添加到数据结构的情况下问题更是这样，因为我们必须适当扩大各类型的结构，是由任何种类协议增加膨胀，所有实例来自另一个参数化接口，因此需要一个接口的状态变量数组。通过观察占空比的变化可以忽略协议检查而增加应用程序的CPU使用率是不可计算的。在一些广泛使用的接口插装，尽管许多其中执行诸如通过无线电传输的数据包处理器密集型任务，对协议检查实际处理负荷低。此接口主要的原因是，调用只发生在从一个模块到另一个路口，不是通常包括在处理主循环。另外，适当设计的低级别部分将回调到地方外部接口（因此我们检查有关协议）在一个长的正在运行的任务，而不是中断处理程序。在我们测试应用程序时一贯坚持该公约。5.2发现错误10运行TinyOS的应用程序和用检查协议编译会在一些应用中发现错误。就本条而言，错误是一个明确的违反接口契约的行为。在许多情况下，应用程序特定的语义是这样的，这些错误是在一个这样或那样的情况下被接纳。事实上，这正是我们所期望的，因为我们测试的应用程序都是TinyOS的某些部分，且已使用了好几年。即便如此，我们相信这些错误应该被发现并修正：有问题的组件可供回收再用的，而且是TinyOS核心的部分。在设计改进TinyOS2.09，10时更正其中的一些问题，证明其有效性。这种微妙的问题可以通过相对简单的协议执行发现的事实来表明，我们的做法有可取之处。在这里，我们描述了最有趣的一些错误。5.2.1分相派遣对TinyOS核心的设计，多到一连接，是一个微妙的错误的来源，特别是对分相操作。如果多个用户线连接到服务接口，那么从一个用户的请求完成事件发送给所有用户。例如，在增量应用中，SendMsg接口提供QueuedSendM组件是由三个不同的组件使用：BCastM，MultiHopEngineM和MultiHopLEPSM。在这种情况下，BCastM、MultiHopEngineM和MultiHopLEPSM是连接到同一个SendMsg接口。该QueuedSendM组件没有信息来确定那三个哪个用户名为SendMsg.send（）。因此，当信号SendMsg.sendDone（）处理程序时，事件要求三个用户。由于QueuedSendM可以有多个未解决的数据包，它有可能超过一个用户有一个数据包在发送队列。因此，其中可能超过一个需要等待SendMsg.sendDone（）。如果用户不检查传递到SendMsg.sendDone（）缓冲事件是它自己的，那么它可能会错误地得出结论：其传输已完成，而数据包仍然在队列中。双方BCastM和MultihopEngineM正确进行检查，除了MultihopLEPSM，这是链路预算的责任，其实不然。因此，它可能是路由航标损坏，造成路由的失败。用我们的工具一样发现了许多错误，这问题不会体现出来，直到应用程序的组件连接在一起。单个nesC的检查和分析检测这里讨论的许多问题是不够的。以上可以在QueuedSendM组件的QueueSendMsg.sendDone（）函数的可靠的C源文件调用和TinySec使用中看到例子。11这似乎是一个与该TinyOS1.X的通讯层和接口层建立多个组织的根本问题，所有使用相同的变量发送数据结构以确定事件路由。这将产生一个漏洞，在构思一个共享组件可以作为一个完全由包括在接口定义的参数内部对待，因为它是在全局可用为前提，其中已经有消息类型定义。此问题已在TinyOS2.0得到解决，通过虚拟发送抽象使用10。5.2.2接口规范不明确之处如果接口没有被明确指定，那么一些实现需要比别人更强的检查方法。这将产生一种情况，目前还不清楚一个接口哪一边是负责检查错误的条件。严格执行对一个组件一个测试可以承担对方的接口执行检查。但是，如果该组件被连接到一个宽松的实现，假设调用者执行的检查，然后问题就会接踵而至。例如，当SendMsg.send（）调用成功，数据包缓冲区的所有权传递给SendMsg提供者。随后SendMsg.sendDone（）事件所有权从SendMsg用户缓冲区返回。当其他组件拥有它时，一个组件来访问缓冲区是错误的。例如，如果用户在SendMsg.send（）成功调用后修改缓冲区，那么它可能会导致数据的有效载荷和预先计算的CRC变得不一致，导致接收者检查失败。有些组件提供SendMsg如AMPromiscuous组件是TinyOS的核心部分，实施额外的检查：由于本组件只能在同一时间传送一个缓冲区，它拒绝多个相同的缓冲区发送。由于重复send（）函数将自动失效，没有读取或写入到缓冲区，而不是多个请求的程序错误的来源。其他实现的SendMsg会接受多个发送请求，特别是QueuedSendM，并在这些情况下，发送多个相同的缓冲区可能危及其完整性。事实上，这个功能被发现时QueuedSendM模块试图通过两次发送单个AMPromiscuous缓冲区，违反了以前的更严格版本的SendMsg的协议。由于在AMPromiscuous没有明确的检查，这并不会导致程序错误，但有趣的是注意到，QueuedSendM组件执行正确的AMPromiscuous操作限制发送，QueuedSendM本身并不受限制。这些不明确之处，也是组件重用的一种障碍，强化协议将允许开发者有更大的信心掌握组件的行为。应该指出的是，TinyOS2.0消除这种不一致，不允许多个发送从同一QueuedSendM版本的AMQueue组件8。5.2.3初始化问题TinyOS操作的原则是每个模块负责初始化和启动它使用的程序。这在设计12共享的低层接口功能时反复初始化，因为所有的模块都使用它们来在线。这显然是低效的，如图11所示，像StdControl接口有许多个初始化/开始警告，这种行为是很普遍的。资源使用状况：无协议/协议设计（增加）数据大小（字节）代码大小（字节）占空比（）警告验证错误BlinkTask52/89(71.1%)1540/1918(26.5%)0.0280/0.0283(1.1%)00CntToLedsAndRfm450/534(18.2%)10572/11476(8.6%)6.310/6.314(0.063%)60Surge1931/2242(16.1%)16196/17306(6.8%)7.789/7.792(0.037%)374SurgeReliable2165/2490(15.0%)21532/22818(6.0%)9.139/9.140(0.013%)425SurgewithTinySec2174/2476(13.9%)24968/27398(4.5%)8.069/8.201(1.64%)476HighFrequencySampling851/944(10.9%)17082/18002(5.4%)5.844/5.845(0.017%)50图10：运行的应用程序与协议动态检查的结果代码行数发现的警告验证发现的错误发送6007计时器5726接受3701安全控制66731模数转换控制47170图11：协议统计。在应用程序的源代码中轻微和严重违反协议情况的警告和错误计数参考。例如，在启动StdControl将多次产生一个警告，StdControl在启动时没有被初始化是一个错误。在CClOOORadioIntM（这是云母平台的无线模块的默认实例）接口中，该组件每次开始将初始化一个单点计时器。由于启动命令一再调用，每一次重新设置单点定时器，本协议在计时器触发前由于滥用会弄错时间。尽管TinyOS不是一个硬性的实时系统，滥用协议是计时器模块不负责任的履行其基本功能，即未能在适当的时间间隔触发事件。虽然根据我们所知的情况这是一个良性的13错误，其中需要精确的计时将会导致错误的调试困难。CClOOORadioIntM重复初始化是一个错误的来源，在Surge、Surge可靠和TinySecSurge，因为他们有相关无线电元件类似的使用。此问题已经被认识到，并在很大程度上涉及TinyOS2.0的分离初始化和模块启动特性9。5.3意外的接口使用我们工作的一个重要结果是确定了接口的语义。在许多情况下，我们已经找到了有点特别的实际的使用情况，和指定一个具体的接口协议，我们发现看似简单的接口有冗余和隐式要求。例如，mica2平台提供了ADCControl接口来控制其模数转换器。为了使用ADC，硬件必须初始化，每个组件本身必须在ADC端口登记，然后可以正常使用ADC。根据给定公约，但是，端口登记应该在在初始化之前。由于ADCControl.bindPort（）命令包含对低级别的初始化函数的隐式调用，所以在初始化之前使用接口和底层硬件是一个明显的错误。隐式的调用也包含在一个全局初始化函数的单独调用，使混乱进一步加剧。这种冗余的结果是，ADCControl初始化每个组件至少使用两个额外的时间，实际的初始化函数必须以这样一种方式来允许端口初始化请求，而并不破坏其状态交叉运行。我们不能根据个人的方便违反这个协议，虽然它是低效的但自成立以来始终被遵守。加强检查常用接口的隐式使用，常常要求显示类似的矛盾和接口为克服怪异的编程困难提供了大量机会。想象一下，开发人员为不同的硬件实现编写一个新的ADCControl。如果他们不知道他们应该期望他们的初始化例程在程序中多次随机被调用，这是他们不太会考虑到这些代码限制它。奇怪的错误会产生。我们希望，我们的协议检查工具将把鼓励的目光投向了这些以前更直接被隐藏的编程问题。6.未来的工作跨协议检查。由于我们的协议是独立的单位，我们不能跨越多个指定接口的约束。例如，尽管使用一个接口的缓冲区可以同时发送和接收是严重错误，我们的协议系统无法检测到这个问题。协议请求超越命令/事件所在模块。我们目前的协议无论什么时候都可以检查一个组件控制流跨越边界。这是不足以检查我们要检查的一些属性。比如，14除了验证我们要检查的应用程序方面的消息缓冲区状态机制，如图7所示，没有一个缓冲区，它没有自己的组件引用。这就要求稽核内存操作：一种改造我们目前的系统方案的微小操作。呼唤死亡的生成。明确协议将使我们能够感受到一个软件组件被验证。使用诸如TOSSIM或Avrora仿真环境，我们希望自动生成单个组件的单元测试。这些单元测试源代码将填入执行中的另一个组件的所有接口。考虑到跟随他们的所有其他组件，这将使我们是否能访问组成如下签订的协议。这种方法类似于死系统的输入，探索了一套完整的可能的输入使用惰性结合，以产生一个输入，导致崩溃1。静态检查。对nesC的模块化特性和TinyOS的应用使得静态检查的想法很有吸引力。尽管大多数嵌入式应用是小型和相对简单的，目前的并行度，使整个程序检查昂贵。然而，检查范围内的各组成部分的合同框架是一个有趣的的可能性，使用存根