Efficient SAT-based bounded model checking for software verification

This paper discusses our methodology for formal analysis and automatic verification of software programs. It is applicable to a large subset of the C programming language that includes pointer arithmetic and bounded recursion. We consider reachability properties, in particular whether certain assertions or basic blocks are reachable in the source code, or whether certain standard property violations can occur. We perform this analysis via a translation to a Boolean circuit representation based on modeling basic blocks. The program is then analyzed by a back-end SAT-based bounded model checker, where each unrolling is mapped to one step in a block-wise execution of the program.     

改进的验证正确性ACTL性质的限界模型检测方法

近些年来,基于SAT的限界模型检测方法作为基于BDD的限界模型检测方法的一种有效补充,已经得到了一定的发展。其中,大部分的研究成果都集中在了使用该方法来进行系统查错方面,而在正确性性质的验证上一直难有突破,原因在于正确性性质的验证依赖于一个完备上界,而这个完备上界在限界模型检测方法中很难实现。对传统限界模型检测中的编码方式进行相应改变,就能够在一定程度上解决这一问题,进行正确性性质的验证。在此基础上对该编码方法进行改进,从而提高它的求解效率,扩大其应用领域。     

Model checking, testing and verification working together

We present a symbolic model checking approach that allows verifying a unit of code, e.g., a single procedure or a collection of procedures that interact with each other. We allow temporal specifications that assert over both the program counters and the program variables. We decompose the verification into two parts: (1) a search that is based on the temporal behavior of the program counters, and (2) the formulation and refutation of a path condition, which inherits conditions constraining the program variables from the temporal specification. This verification approach is modular, as we do not require that all the involved procedures are provided. Furthermore, we do not request that the code is based on a finite domain. The presented approach can also be used for automating the generation of test cases for unit testing.A preliminary version of the paper, with the title Unit Checking: Symbolic Model Checking for a Unit of Code appears in the Lecture Notes in Computer Science volume 2772, Verification– Theory and Practice, celebrating Zohar Manna’s 64th birthdayThis research was partially supported by US Army Research Office Grant number DAAAD19-01-1-0473This research was partially supported by Subcontract UTA03-031 to The University of Warwick under University of Texas at Austin’s prime National Science Foundation Grant #CCR-0205483Received February 2004Revised September 2004 and April 2005Accepted April 2005 by M. Leuschel and D. J. Cooke     

HySAT: An efficient proof engine for bounded model checking of hybrid systems

In this paper we present HySAT, a bounded model checker for linear hybrid systems, incorporating a tight integration of a DPLL–based pseudo–Boolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT, ICS, or CVC, our tool exploits the various optimizations that arise naturally in the bounded model checking context, e.g.isomorphic replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate that those optimizations are crucial to the performance of the tool.     

一种无线传感器软件非接触升级的方法

基于MSP430无线传感器系统,设计了一种无线传感器软件非接触升级的方法.该方法充分利用现有资源,不需要传感器而是通过程序下载线与计算机相联,稳定可靠地完成了无线传感器应用程序的升级更新.该方法对于Flash可系统编程的其他系列单片机系统同样适用,具有很好的实用性和通用性.     

新型传感器节点物理层TPHY协议设计与实现

无线传感器网络是当前国际上备受关注的前沿热点研究领域。由于无线传感节点的计算能力、存储能力、通信能力和携带能量都十分有限,因此对网络协议提出了更高的要求。本文在基于CC2420射频芯片设计的GAINZ无线传感节点上,设计并实现了基于TinyOS系统的IEEE802.15.4规范物理层协议TPHY(TinyOS-PHY),提供了无线分组收发、信道能量检测、链路质量指示、空闲信道评估、信道频率选择、激活和休眠射频收发器的功能。测试结果表明基于该方案设计实现的物理层具有误码率低、抗干扰性强、可靠性高和耗能少的优点。     

Embedded software verification in hardware–software codesign

Concurrent Embedded Real-Time Software (CERTS) is intrinsically different from traditional, sequential, independent, and temporally unconstrained software. The verification of software is more complex than hardware due to inherent flexibilities (dynamic behavior) that incur a multitude of possible system states. The verification of CERTS is all the more difficult due to its concurrency and embeddedness. The work presented here shows how the complexity of CERTS verification can be reduced significantly through answering common engineering questions such as when, where, and how one must verify embedded software. First, a new Schedule-Verify-Map strategy is proposed to answer the when question. Second, verification under system concurrency is proposed to answer the where question. Finally, a complete symbolic model checking procedure is proposed for CERTS verification. Several application examples illustrate the usefulness of our technique in increasing verification scalability.     

Formal verification of software source code through semi-automatic modeling

We describe the experience of modeling and formally verifying a software cache algorithm using the model checker RuleBase. Contrary to prevailing wisdom, we used a highly detailed model created directly from the C code itself, rather than a high-level abstract model.     

带移动节点的无线传感器网络时间同步方法

为提高无线传感器网络中节点间时间同步的精度并且降低节点能量消耗,提出了一种基于移动节点与静态节点混合网络的时间同步方法.先建立一个带移动的节点的分簇网络结构,再结合发送者一接受者与改进的发送者一发送者两种同步模型从多个移动节点同时发起同步.通过数学分析和仿真得出该同步方法在同步时间精度和节点节能方面具有良好的性能.     

Real-time scheduling for energy harvesting sensor nodes

Energy harvesting has recently emerged as a feasible option to increase the operating time of sensor networks. If each node of the network, however, is powered by a fluctuating energy source, common power management solutions have to be reconceived. This holds in particular if real-time responsiveness of a given application has to be guaranteed. Task scheduling at the single nodes should account for the properties of the energy source, capacity of the energy storage as well as deadlines of the single tasks. We show that conventional scheduling algorithms (like e.g. EDF) are not suitable for this scenario. Based on this motivation, we have constructed optimal scheduling algorithms that jointly handle constraints from both energy and time domain. Further we present an admittance test that decides for arbitrary task sets, whether they can be scheduled without deadline violations. To this end, we introduce the concept of energy variability characterization curves (EVCC) which nicely captures the dynamics of various energy sources. Simulation results show that our algorithms allow significant reductions of the battery size compared to Earliest Deadline First scheduling.

自适应软件动态过程时间特性建模与验证方法

现有自适应软件建模与验证方法较少考虑时间约束,然而,在时间攸关应用领域,自适应软件能否正确运行,不仅要考虑自适应逻辑的正确性,还要考虑自适应软件动态过程的时间特性。为此,首先显式定义了自适应软件的时间特性（监控周期、延迟触发时间、自适应过程截止时间、自适应调节时间和稳定时间等）;然后,构造了一种基于时间自动机网络（TAN）的自适应软件动态过程时间特性建模模板;最后,将自适应软件时间特性描述为定时计算树逻辑（TCTL）的形式,并对时间特性进行了形式化分析和验证。结合具体案例验证了该自适应软件时间特性建模和验证方法,结果表明该方法能够显式刻画自适应软件时间特性,降低其形式化建模的难度。     

基于MSP430微处理器的低功耗无线传感器网络节点设计

针对目前温度、湿度等数据采集监测系统功耗大、应用场合有限等缺陷．设计一种基于MSP430系列微处理器的低功耗无线传感器节点。硬件设计基于Moteiv方案,采用超低功耗单片机MSP430F1611作为数据处理芯片,以CC2420无线射频芯片作为收发芯片,并拥有JTAG以及其他扩展接口。通过合理设计电路来降低设备功耗,提高设备的能量利用率,从而达到提高无线传感器网络的稳定性和可靠性,延长网络生命周期的目的。     

基于MSP430的磁弹性传感器检测系统设计

磁弹性传感器无线无源的优点使其在无损检测、在体分析等领域具有非常广阔的应用前景.通过对磁弹性传感器检测原理的分析,设计了一种基于MSP430平台的小型化磁弹性传感器检测系统.该系统以MSP430单片机为控制核心,利用永磁铁作为偏置磁场激励,集成了交流激励信号产生单元、有效值检测单元和AD采样单元,并通过RS-232实现与上位机之间的通信.实验结果表明:该检测系统可以方便快捷地实现对磁弹性传感器共振特性的检测,具有稳定性好、集成度高、功耗低的特点,能够满足磁弹性传感器在不同状态和环境下共振特性的精确检测需求.     

一种低功耗无线传感器网络节点设计

无线传感网络节点功耗直接决定了无线网络的生存周期,为了降低节点能耗,在对多种微处理器芯片和射频芯片性能分析比较的基础上,选择了MSP430F2618处理器芯片和射频芯片CC2520射频芯片,采用微处理器与无线模块独立架构,设计了一种性能灵活无线网络节点;提出了微处理器、射频芯片在工作模式与多种低功耗模式之间切换,以及微处理器时钟的控制等节能策略,在此基础上设计了网络路由节点和端节点软件系统;实验证明:在发射功率为0 dBm,数据传输速率为1 MHz时,设计的节点运行电流和休眠电流(26.1 mA,1.57μA)与传统的Imote节点(35.1 mA,3.6μA)、Mica2节点(56.2 mA,21μA)相比,明显低于传统节点;当节点电池容量为2*700 mAh,工作周期为10分钟时,其生存周期为7.2个月;设计的节点的寿命达到预期目标。     

基于MSP430的纸张挺度测试仪的设计

纸张挺度测试仪用于造纸行业中对纸张试样抗弯曲强度的精确测量,以便于在造纸流程中对纸样质量的实时控制.本文介绍了测试仪的工作原理,利用MSP430单片机设计出新型的精度为1/1000的纸张挺度测试装置,分析了该装置中单片机控制步进电机中断和A/D采样转换中断产生的冲突和对测试结果的影响以及改进办法,并且实现了Huffman压缩算法对采样数据的压缩并传输到上位计算机.目前,改装置已用于工业实践,工作稳定,可靠.     

A survey of recent advances in SAT-based formal verification

Dramatic improvements in SAT solver technology over the last decade and the growing need for more efficient and scalable verification solutions have fueled research in verification methods based on SAT solvers. This paper presents a survey of the latest developments in SAT-based formal verification, including incomplete methods such as bounded model checking and complete methods for model checking. We focus on how the surveyed techniques formulate the verification problem as a SAT problem and how they exploit crucial aspects of a SAT solver, such as application-specific heuristics and conflict-driven learning. Finally, we summarize the noteworthy achievements in this area so far and note the major challenges in making this technology more pervasive in industrial design verification flows.     

Hardware support for memory protection in sensor nodes

With reference to the typical hardware configuration of a sensor node, we present the architecture of a memory protection unit (MPU) designed as a low-complexity addition to the microcontroller. The MPU is aimed at supporting memory protection and the privileged execution mode. It is connected to the system buses, and is seen by the processor as a memory-mapped input/output device. The contents of the internal MPU registers specify the composition of the protection contexts of the running program in terms of access rights for the memory pages. The MPU generates a hardware interrupt to the processor when it detects a protection violation. The proposed MPU architecture is evaluated from a number of salient viewpoints, which include the distribution, review and revocation of access permissions, and the support for important memory protection paradigms, including hierarchical contexts and protection rings.     

Post-order based routing & transport protocol for wireless sensor networks

In this paper, we propose a lightweight, application independent transport protocol for communication of the nodes belonging to a wireless sensor network (WSN) with the nodes belonging to a local area network. The framework consists of a novel downstream routing scheme and a well-known tree based upstream routing protocol for WSNs. The downstream routing protocol leverages Post-order Numbering (PN) of sensor nodes in the collection tree network formed and maintained by the upstream routing protocol. Through the proposed transport framework, using a technique similar to NATing, we achieve a seamless integration of WSNs and IP networks. The proposed protocol was not only evaluated by extensive simulations, but also implemented on a real test bed to show its practical deployability. We built our test bed around a small Wireless Distribution System (WDS) consisting of two laptop computers and eight Micaz motes attached with MTS300 sensor boards. We connected one of the computers in WDS via Ethernet to the LAN while the other operated as a server with a serial forwarder. A gateway board was attached to the second computer via a USB port which enabled it to function also as a base station for the WSN. A distinct advantage of the proposed framework is that an IP client can directly communicate with a sensor node through its base station.     

On automatic verification of self-stabilizing population protocols

The population protocol model has emerged as an elegant computation paradigm for describing mobile ad hoc networks, consisting of a number of mobile nodes that interact with each other to carry out a computation. The interactions of nodes are subject to a fairness constraint. One essential property of population protocols is that all nodes must eventually converge to the correct output value (or configuration). In this paper, we aim to automatically verify self-stabilizing population protocols for leader election and token circulation in the Spin model checker. We report our verification results and discuss the issue of modeling strong fairness constraints in Spin.