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.
As wireless sensor networks (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 producing high-assurance and reliable software for 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. To fill this gap, the project aimed to 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 also aimed to develop a synthesis tool that manipulates the given abstract distributed programs for the automated addition of desired level of fault-tolerance. We achieved the following tasks for addressing the project's goals: 1) Developing useful transformations from distributed system models to wireless networked systems. 2) Developing the middleware services required for the transformation. 3) Automated synthesis of fault-tolerance. The major impact from our task on developing useful transformations were the findings that 1) message losses in the concrete WSNs model penalizes the performance of the transformed program severely, and 2) by identifying and deliberately designing slow actions at the abstract level we can improve the performance of the transformed program asymptotically. (Slow actions mean that the process can tolerate slightly stale state from other processes, which enables the concrete system to be more loosely-coupled, and tolerate communication problems better.) The major impact from our task on developing middleware services for the transformation was the finding that by restricting the state updates to be only local at the node, rather than allowing a direct write to the states of neighboring nodes, we can obtain a useful and very efficient, fast subset of our earlier distributed transaction implementation on WSANs. Another major finding was that the results in our work have the potential to apply to scenarios in distributed systems to expedite the execution of distributed protocols. In particular, recent research has focused on expediting execution of distributed protocols by reducing wait involved in different actions. However, the work in this context is focused on the use of syntactic information and therefore is limited in its application. Our work on partitioning of slow fast actions is semantic in nature and, hence is expected to have a wider application. The major impact from our task on automated synthesis of fault-tolerance is that we can achieve orders of magnitude reductions in the cost of verification by suitably decomposing the algorithm and exploiting the symmetry of nodes' programs in WSNs. More recently we found that the slow-fast action idea transcends the WSN model and provides similar performance improvements and developer-friendly features in the cloud computing systems domain, particularly for processing of large-scale graph applications. This project supported training and education of two graduate students: Serafettin Tasci and Bahadir Ismail Aydin. This project also resulted in several conference and journal publications. A list of publications and more details are available at: www.cse.buffalo.edu/~demirbas/Prose/index.html
