More Web Proxy on the site http://driver.im/

Article

Incremental synthesis of fault-tolerant real-time programs

Authors:

Borzoo Bonakdarpour,

Sandeep S. KulkarniAuthors Info & Claims

SSS'06: Proceedings of the 8th international conference on Stabilization, safety, and security of distributed systems

Pages 122 - 136

Published: 17 November 2006 Publication History

Abstract

In this paper, we focus on the problem of automated addition of fault tolerance to an existing fault-intolerant real-time program. We consider three levels of fault-tolerance, namely nonmasking, failsafe, and masking, based on safety and liveness properties satisfied in the presence of faults. More specifically, a nonmasking (respectively, failsafe, masking) program satisfies liveness (respectively, safety, both safety and liveness) in the presence of faults. For failsafe and masking fault-tolerance, we consider two additional levels, soft and hard, based on satisfaction of timing constraints in the presence of faults. We present a polynomial time algorithm (in the size of the input program's region graph) that adds bounded-time recovery from an arbitrary given set of states to another arbitrary set of states. Using this algorithm, we propose a sound and complete synthesis algorithm that transforms a fault-intolerant real-time program into a nonmasking fault-tolerant program. Furthermore, we introduce sound and complete algorithms for adding soft/hard-failsafe fault-tolerance. For reasons of space, our results on addition of soft/hard-masking fault-tolerance are presented in a technical report.

References

[1]

M. Pandya and M. Malek. Minimum achievable utilization for fault-tolerant processing of periodic tasks. IEEE Transations on Computers, 47(10):1102-1112, 1998.

Digital Library

[2]

D. Mossé, R. G. Melhem, and S. Ghosh. A nonpreemptive real-time scheduler with recovery from transient faults and its implementation. IEEE Transactions on Software Engineering, 29(8):752-767, 2003.

Digital Library

[3]

B. Bonakdarpour and S. S. Kulkarni. Automated incremental synthesis of timed automata. In International Workshop on Formal Methods for Industrial Critical Systems (FMICS), 2006.

Digital Library

[4]

K. M. Chandy and J.Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.

Digital Library

[5]

A. Ebnenasir, S. S. Kulkarni, and B. Bonakdarpour. Revising UNITY programs: Possibilities and limitations. In 9th International Conference on Principles of Distributed Systems (OPODIS), 2005.

Digital Library

[6]

S. S. Kulkarni and A. Arora. Automating the addition of fault-tolerance. In Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), pages 82-93, 2000.

Digital Library

[7]

S. S. Kulkarni, A. Arora, and A. Chippada. Polynomial time synthesis of Byzantine agreement. In 20th Symposium on Reliable Distributed Systems (SRDS), pages 130-140, 2001.

[8]

S. S. Kulkarni and A. Ebnenasir. Automated synthesis of multitolerance. In International Conference on Dependable Systems and Networks (DSN), pages 209-219, 2004.

Digital Library

[9]

P. C. Attie, A. Arora, and E. A. Emerson. Synthesis of fault-tolerant concurrent programs. ACM Transactions on Programming Languages and Systems, 26(1):125-185, 2004.

Digital Library

[10]

E. Asarin, O. Maler, A. Pnueli, and J. Sifakis. Controller synthesis for timed automata. In IFAC Symposium on System Structure and Control, pages 469-474, 1998.

[11]

E. Asarin and O. Maler. As soon as possible: Time optimal control for timed automata. In Hybrid Systems: Computation and Control (HSCC), pages 19-30, 1999.

Digital Library

[12]

D. D'Souza and P. Madhusudan. Timed control synthesis for external specifications. In 19th Annual Symposium on Theoretical Aspects of Computer Science (STACS), pages 571-582, 2002.

Digital Library

[13]

P. Bouyer, D. D'Souza, P. Madhusudan, and A. Petit. Timed control with partial observability. In Computer Aided Verification (CAV), pages 180-192, 2003.

[14]

L. de Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga. The element of surprise in timed games. In 14th International Conference on Concurrency Theory (CONCUR), 2003.

[15]

M. Faella, S. LaTorre, and A. Murano. Dense real-time games. In Logic in Computer Science (LICS), pages 167-176, 2002.

Digital Library

[16]

R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2-34, 1993.

Digital Library

[17]

R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183- 235, 1994.

Digital Library

[18]

Y. Abdeddam. Scheduling with Timed Automata. PhD thesis, INPG, Grenoble, November 2002.

[19]

B. Bonakdarpour and S. S. Kulkarni. Automatic addition of fault-tolerance to real-time programs. Technical Report MSU-CSE-06-13, Department of Computer Science and Engineering, Michigan State University, 2006.

[20]

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.

Digital Library

[21]

T. A. Henzinger. Sooner is safer than later. Information Processing Letters, 43(3):135-141, 1992.

Digital Library

[22]

B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21:181- 185, 1985.

[23]

A. Arora and M. G. Gouda. Closure and convergence: A foundation of fault-tolerant computing. IEEE Transactions on Software Engineering, 19(11):1015-1027, 1993.

Digital Library

[24]

C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-time systems. In Computer-Aided Verificaion (CAV), pages 399-409, 1991.

Digital Library

Cited By

Bonakdarpour BKulkarni S(2012)Automated model repair for distributed programsACM SIGACT News10.1145/2261417.226143743:2(85-107)Online publication date: 11-Jun-2012
https://dl.acm.org/doi/10.1145/2261417.2261437
Bonakdarpour BLin YKulkarni SChakraborty SJerraya ABaruah SFischmeister S(2011)Automated addition of fault recovery to cyber-physical component-based modelsProceedings of the ninth ACM international conference on Embedded software10.1145/2038642.2038663(127-136)Online publication date: 9-Oct-2011
https://dl.acm.org/doi/10.1145/2038642.2038663
Bonakdarpour BKulkarni SChakraborty SHalbwachs N(2009)Compositional verification of fault-tolerant real-time programsProceedings of the seventh ACM international conference on Embedded software10.1145/1629335.1629341(29-38)Online publication date: 12-Oct-2009
https://dl.acm.org/doi/10.1145/1629335.1629341
Show More Cited By

Recommendations

Synthesizing bounded-time 2-phase fault recovery
Abstract
We focus on synthesis techniques for transforming existing fault-intolerant real-time programs into fault-tolerant programs that provide phased recovery. A fault-tolerant program is one that satisfies its safety and liveness specifications as well ...
Disassembling real-time fault-tolerant programs
EMSOFT '08: Proceedings of the 8th ACM international conference on Embedded software

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 ...
Automated Synthesis of Multitolerance
DSN '04: Proceedings of the 2004 International Conference on Dependable Systems and Networks

We concentrate on automated synthesis of multitolerant programs,i.e., programs that tolerate multiple classes of faultsand provide a (possibly) different level of fault-tolerance toeach class. We consider three levels of fault-tolerance: (1)failsafe, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SSS'06: Proceedings of the 8th international conference on Stabilization, safety, and security of distributed systems

November 2006

589 pages

ISBN:9783540490180

Editors:
Ajoy K. Datta
School of Computer Science, University of Nevada Las Vegas, Las Vegas
,
Maria Gradinariu
Universite Paris 6, LIP6, Paris, France

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 17 November 2006

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bonakdarpour BKulkarni S(2012)Automated model repair for distributed programsACM SIGACT News10.1145/2261417.226143743:2(85-107)Online publication date: 11-Jun-2012
https://dl.acm.org/doi/10.1145/2261417.2261437
Bonakdarpour BLin YKulkarni SChakraborty SJerraya ABaruah SFischmeister S(2011)Automated addition of fault recovery to cyber-physical component-based modelsProceedings of the ninth ACM international conference on Embedded software10.1145/2038642.2038663(127-136)Online publication date: 9-Oct-2011
https://dl.acm.org/doi/10.1145/2038642.2038663
Bonakdarpour BKulkarni SChakraborty SHalbwachs N(2009)Compositional verification of fault-tolerant real-time programsProceedings of the seventh ACM international conference on Embedded software10.1145/1629335.1629341(29-38)Online publication date: 12-Oct-2009
https://dl.acm.org/doi/10.1145/1629335.1629341
Bonakdarpour BKulkarni SArora Ade Alfaro LPalsberg J(2008)Disassembling real-time fault-tolerant programsProceedings of the 8th ACM international conference on Embedded software10.1145/1450058.1450082(169-178)Online publication date: 19-Oct-2008
https://dl.acm.org/doi/10.1145/1450058.1450082
Bonakdarpour B(2008)Challenges in transformation of existing real-time embedded systems to cyber-physical systemsACM SIGBED Review10.1145/1366283.13662945:1(1-2)Online publication date: 1-Jan-2008
https://dl.acm.org/doi/10.1145/1366283.1366294
Bonakdarpour BKulkarni SAbujarad F(2007)Distributed synthesis of fault-tolerant programs in the high atomicity modelProceedings of the 9h international conference on Stabilization, safety, and security of distributed systems10.5555/1785110.1785115(21-36)Online publication date: 14-Nov-2007
https://dl.acm.org/doi/10.5555/1785110.1785115

View Options

View options

Media

Figures

Other

Tables

View Table of Contents