Disassembling real-time fault-tolerant programs

ABSTRACT

We focus on decomposition of hard-masking real-time fault-tolerant programs (where safety, timing constraints, and liveness are preserved in the presence of faults) that are designed from their fault-intolerant versions. Towards this end, motivated by the concepts of state predicate detection and state predicate correction, we identify three types of fault-tolerance components, namely, detectors, weak S-correctors, and strong S-correctors. We show that any hard-masking program can be decomposed into its fault-intolerant version plus a collection of detectors, and, weak and strong S-correctors. We argue that such decomposition assists in providing assurance about dependability and time-predictability of embedded systems.

REFERENCES

• 1: B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21:181--185, 1985.
• 2: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 3: R. Alur and T. A. Henzinger. Real-time system = discrete system + clock variables. International Journal on Software Tools for Technology Transfer, 1(1-2):86--109, 1997.
• 4: Anish Arora , Sandeep S. Kulkarni, Component Based Design of Multitolerant Systems, IEEE Transactions on Software Engineering, v.24 n.1, p.63-78, January 1998 [doi>10.1109/32.663998]
• 5: A. Arora , S. S. Kulkarni, Detectors and Correctors: A Theory of Fault-Tolerance Components, Proceedings of the The 18th International Conference on Distributed Computing Systems, p.436, May 26-29, 1998
• 6: B. Bonakdarpour and S. S. Kulkarni. Incremental synthesis of fault-tolerant real-time programs. In International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), LNCS 4280, pages 122--136, 2006.
• 7: Borzoo Bonakdarpour , Sandeep S. Kulkarni, Masking Faults While Providing Bounded-Time Phased Recovery, Proceedings of the 15th international symposium on Formal Methods, May 26-30, 2008, Turku, Finland [doi>10.1007/978-3-540-68237-0_26]
• 8: Tushar Deepak Chandra , Vassos Hadzilacos , Sam Toueg, The weakest failure detector for solving consensus, Journal of the ACM (JACM), v.43 n.4, p.685-722, July 1996 [doi>10.1145/234533.234549]
• 9: Tushar Deepak Chandra , Sam Toueg, Unreliable failure detectors for reliable distributed systems, Journal of the ACM (JACM), v.43 n.2, p.225-267, March 1996 [doi>10.1145/226643.226647]
• 10: A. Ebnenasir and B. H. C. Cheng. Architecting Dependable Systems IV, chapter A Pattern-Based Approach for Modeling and Analyzing Error Recovery, pages 115--141. Springer Berlin / Heidelberg, 2007.
• 11: F. C. Gärtner and A. Jhumka. Automating the addition of fail-safe fault-tolerance: Beyond fusion-closed speci¯cations. In FORMATS/FTRTFT, pages 183--198, 2004.
• 12: Sukumar Ghosh , Xin He, Fault-containing self-stabilization using priority scheduling, Information Processing Letters, v.73 n.3-4, p.145-151, Feb.29.2000 [doi>10.1016/S0020-0190(00)00006-5]
• 13: Thomas A. Henzinger, Sooner is safer than later, Information Processing Letters, v.43 n.3, p.135-141, Sept. 14, 1992 [doi>10.1016/0020-0190(92)90005-G]
• 14: A. Jhumka, F. Gartner, C. Fetzer, and N. Suri. On systematic design of fast and perfect detectors. Technical Report 200263, School of Computer and Communication Sciences, EPFL, 2002.
• 15: Arshad Jhumka , Martin Hiller , Neeraj Suri, Component-Based Synthesis of Dependable Embedded Software, Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Co-sponsored by IFIP WG 2.2, p.111-128, September 09-12, 2002
• 16: Sandeep Sadashiv Kulkarni , Anish Arora, Component based design of fault-tolerance, The Ohio State University, 1999
• 17: Sandeep S. Kulkarni , Ali Ebnenasir, Automated Synthesis of Multitolerance, Proceedings of the 2004 International Conference on Dependable Systems and Networks, p.209, June 28-July 01, 2004
• 18: Sandeep S. Kulkarni , John M. Rushby , Natarajan Shankar, A case-study in component-based mechanical verification of fault-tolerant programs, Workshop on Self-stabilizing Systems, p.33-40, June 05, 1999
• 19: John M. Rushby, An Overview of Formal Verification for the Time-Triggered Architecture, Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Co-sponsored by IFIP WG 2.2, p.83-106, September 09-12, 2002
• 20: Oliver E. Theel , Felix C. Gärtner, An exercise in proving convergence through transfer functions, Workshop on Self-stabilizing Systems, p.41-47, June 05, 1999

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability
          Subjects: Verification

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability
          Subjects: Fault-tolerance
      D.4.7 Organization and Design
          Subjects: Real-time systems and embedded systems

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

General Terms:
Reliability, Theory, Verification

Keywords:
bounded-time recovery, component-based analysis, decomposition, fault-tolerance, formal methods, real-time