Tool Support for Producing High Assurance and Reliable Software for Wireless Sensor Actor Networks

Software Engineering and Network Systems Laboratory
Department of Computer Science and Engineering
Michigan State University

Principal Investigators : Murat Demirbas and Sandeep Kulkarni

Proposal Summary

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.

Publications related to this Project (available from here)

q Jingshu Chen, Fuad Abujarad, Sandeep S. Kulkarni: Towards scalable model checking of self-stabilizing programs. J. Parallel Distrib. Comput. 73(4): 400-410 (2013)

q Jingshu Chen, Sandeep S. Kulkarni: MR4UM: A framework for adding fault tolerance to UML state diagrams. Theor. Comput. Sci. 496: 17-33 (2013)

q Ali Ebnenasir, Reza Hajisheykhi, Sandeep S. Kulkarni: Facilitating the design of fault tolerance in transaction level SystemC programs.Theor. Comput. Sci. 496: 50-68 (2013)

q Jingshu Chen, Sandeep S. Kulkarni: SMT-Based Model Checking for Stabilizing Programs^,. ICDCN 2013: 393-407

q Yiyan Lin, Borzoo Bonakdarpour, Sandeep S. Kulkarni: Automated Addition of Fault-Tolerance under Synchronous Semantics. SSS 2013: 266-280

q Reza Hajisheykhi, Ali Ebnenasir, Sandeep S. Kulkarni: Modeling and Analyzing Timing Faults in Transaction Level SystemC Programs. SSS 2013: 344-347

q Jingshu Chen, Sandeep S. Kulkarni: SMT-Based Model Checking for Stabilizing Programs^,. International Conference on Distributed Systems and Networks 2013: 393-407

q Borzoo Bonakdarpour, Sandeep S. Kulkarni, Fuad Abujarad: Symbolic synthesis of masking fault-tolerant distributed programs. Distributed Computing 25(1): 83-108 (2012)

q Borzoo Bonakdarpour, Sandeep S. Kulkarni: Automated model repair for distributed programs. SIGACT News 43(2): 85-107 (2012)

q Fuad Abujarad, Sandeep S. Kulkarni: Automated constraint-based addition of nonmasking and stabilizing fault-tolerance. Theor. Comput. Sci. 412(33): 4228-4246 (2011)

q Murat Demirbas, Serafettin Tasci, Sandeep S. Kulkarni: Maestro: A cloud computing framework with automated locking. ISCC 2012: 833-838

q Jingshu Chen, Sandeep S. Kulkarni: Brief Announcement: Verification of Stabilizing Programs with SMT Solvers. SSS 2012: 179-182

q Jingshu Chen, Sandeep S. Kulkarni: Application of Automated Revision for UML Models: A Case Study. ICDCN 2012: 31-45

q Ali Ebnenasir, Reza Hajisheykhi, Sandeep S. Kulkarni: Facilitating the Design of Fault Tolerance in Transaction Level SystemC Programs. ICDCN 2012: 91-105

q Yiyan Lin and Sandeep Kulkarni. Automatic Generation of Graceful Programs. 31st IEEE International Symposium on Reliable Distributed Systems (SRDS) 2012. Irvine, California.

q Borzoo Bonakdarpour and Sandeep Kulkarni. Active Stabilization. International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS) 2011, Grenoble, France.

q Borzoo Bonakdarpour, Yiyan Lin and Sandeep Kulkarni. Automated Addition of Fault Recovery to Cyber-physical Component-based Models. ACM International Conference on Embedded Software (EMSOFT) 2011, Taipei, Taiwan.

q Mahesh Arumugam, Murat Demirbas and Sandeep Kulkarni. ``Slow is fast'' for Wireless Sensor Networks in the Presence of Message Losses, The 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems, 2010.

q Sandeep Kulkarni, Fuad Abujarad: Weakest Invariant Generation for Automated Addition of Fault-Tolerance, Electronic Notes in Theoretical Computer Science, 2009

q Fuad Abujarad, Sandeep Kulkarni, . Constraint Based Automated Synthesis of Nonmasking and Stabilizing Fault-Tolerance, Theoretical Computer Science, 2010

q Jingshu Chen and Sandeep Kulkarni Effectiveness of Fairness in Verification of Self-stabilizing Programs, OPODIS 2010

q Fuad AbuJarad Complexity Issues in Automated Model Revision Without Explicit Legitimate States The 12th International Symposium on Stabilization, Safety, and Security of Distributed Systems, 2010.

q Fuad Abujarad Towards Automated Model Revision for Fault-tolerant Systems, PhD Dissertation, Michigan State University.

Tools related to this Project (available from here)

q SYCRAFT: A tool for automated addition of fault-tolerance.

q SFTransform: A tool for transformation of distributed protocols into sensor network model with the use of SF shared memory model.

This material is based upon work supported by the National Science Foundation under Grant No. 0914913. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation (NSF)