CSR: Small: Collaborative Research: Tool Support for Producing High Assurance and Reliable Software for Wireless Sensor Actor Networks

无线传感器网络(WSN)主要用于数据收集目的，还没有被用于任何一致性或安全关键应用的环境中。因此，无线传感器网络的软件开发大多是在尽最大努力的基础上完成的。然而，随着无线传感器网络越来越多地与驱动能力相结合，由此产生的无线传感器作用器网络(WSAN)需要更多的保证和生存性保证。这个项目的目标是设计和实现实现WSAN软件保证和可靠性所需的工具支持。该项目将产生一个转换工具，允许WSAN程序以传统上用于描述抽象分布式程序的高级模型编写，并自动将这些抽象程序转换为部署在WSAN中的程序，同时保持其正确性和可靠性属性。该项目还将开发一个综合工具，该工具可以操作给定的抽象分布式程序，以自动添加所需的容错级别。最后，该项目将设计一个框架，防止在具体系统中引入辅助状态的破坏，以确保部署的程序是可验证的可靠的。该项目将简化高保证WSANS软件的开发，并有可能为高保证网络物理系统的开发铺平道路。该项目将通过开发课程、建立和传播系统软件以及向更广泛的社区宣传，将研究和教育结合起来。

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.