Wireless sensor networks (WSNs) have been mainly used for data collection purposes, and have not been employed in the context of any consistency- or safety-critical applications. As such software development for WSNs has been done mostly on a best-effort basis. However, as WSNs get more integrated with actuation capabilities, the resulting wireless sensor actor networks (WSANs) require more assurance and survivability guarantees. The goal of this project is to design and implement the tool-support necessary for achieving assurance and reliability of WSANs software.
The project will produce a transformation tool that allows programs for WSANs to be written in high-level models traditionally used to describe abstract distributed programs and automatically transforms these abstract programs, while preserving their correctness and reliability properties, into programs deployed in WSANs. The project will also develop a synthesis tool that manipulates the given abstract distributed programs for the automated addition of desired level of fault-tolerance. Finally, the project will design a framework that guards against the corruption of the auxiliary state introduced at the concrete system to ensure that the deployed program is verifiably reliable.
This project will simplify the development of high assurance WSANs software, and has the potential to pave the way to high assurance cyber-physical systems development. The project will integrate research and education through coursework development, building and dissemination of systems software, and outreach to the wider community.
Award 0914913 - Outcomes Report PIs: Murat Demirbas (SUNY Buffalo) and Sandeep Kulkarni (Michigan State University) Our project proposed to build tool support for producing high-assurance and reliable software for wireless sensor/actor networks (WSANs). The main challenge in addressing this problem is that the high-level models considered in developing and verifying distributed systems do not account for the challenges and opportunities in wireless networks. The goals of our project were as follows: Design of algorithms that allow traditional distributed computing programs to be deployed in sensor networks while preserving correctness and fault-tolerance properties. Development of algorithms and tools for automated synthesis to support manipulation of abstract programs into programs that tolerate desired faults A fault-tolerance preserving framework that guards against the corruption of the auxiliary state introduced at the concrete system to ensure that the deployed program is verifiably reliable. To achieve these goals, we conducted research in the area of sensor networks, formal methods, and distributed systems. The main accomplishments of this work are as follows: Developing useful transformations to wireless networked systems We investigated models for the concrete WSNs that takes into account the energy-efficiency requirements and message loss characteristics of the concrete system. We identified that existing transformations from high-level abstract distributed systems models to WSNs quickly become inefficient in the presence of prevalent message losses in WSNs, and this prohibits their wider adoption. To address this problem, we proposed a variation of the high-level shared memory model, the 'SF' shared memory model, where the actions of each node are partitioned into 'slow' actions and 'fast' actions. The traditional shared memory model consists only of fast actions and a lost message can disable the nodes from execution. Slow actions, on the other hand, enable the nodes to use slightly stale state from other nodes, so a message loss does not prevent the node from execution. We quantified over the advantages of using slow actions under environments with varying message loss probabilities, and find that a slow action has asymptotically better chance of getting executed than a fast action when the message loss probability increases. We also presented guidelines for helping the protocol designer identify which actions can be marked as slow so as to enable the transformed program to be more loosely-coupled, and tolerate communication problems (latency, loss) better. We have developed algorithms for utilizing parallelism and symmetry during automated revision of WSN programs. In particular, in this work, we focused on parallelizing the task involved in addition of fault-tolerance with the use of multiple threads. We found that parallelism that relies on independent behavior of nodes (such as those in WSNs) provides a significant benefit in reducing the time for revision. We have also found that symmetry that utilizes the observation that code of different sensors is 'almost identical' can also significantly reduce the time for revision. We have also extended our work on applying the problem of revision with SCR toolset. Specifically, we have developed rules for transforming SCR specification into input to our synthesis tool and utilize it to generate a revised SCR specification that provides fault-tolerance requirements. We have further utilized these results in revision of UML models and SystemC TLM programs. We have also focused on utilizing our work in developing scalable approaches for verifying self-stabilization. In particular, this approach relies on decomposition of the algorithm to reduce the cost of verification by orders of magnitude. Furthermore, to make the revision of sensor network programs, we have developed a new approach for reducing the task of the designer thereby make it easier to apply it in practice. One of the assumptions in formal methods to verify and revise fault-tolerant programs is that it is possible to model faults using transition systems. While this conjecture holds in several examples, it has not been studied in detail. For this reason, we focused on evaluating this conjecture. Specifically, we began with the work of Basic Concepts and Taxonomy of Dependable and Secure Computing. IEEE Trans. Dependable Sec. Comput. 1(1): 11-33 (2004) that characterizes faults from a practitioner's point of view. This work characterizes faults into 31 overlapping categories. We focused on analyzing these faults and the possibility of modeling them using transition systems. This work supported training and education of four graduate students, Jingshu Chen, Fuad Abujarad, Reza Hajishey and Yiyan Lin. Fuad and Jingshu have graduated with PhD. And, Reza and Yiyan are continuing their PhD program. Additional details about the project (including publications and tools) are available at www.cse.msu.edu/~sandeep/projects/sensornet/
