zbMATH — the first resource for mathematics

The complexity of automated addition of fault-tolerance without explicit legitimate states. (English) Zbl 1331.68031
Summary: Existing algorithms for automated model repair for adding fault-tolerance to fault-intolerant models incur an impediment that designers have to identify the set of legitimate states of the original model. This set determines states from where the original model meets its specification in the absence of faults. Experience suggests that of the inputs required for model repair, identifying such legitimate states is the most difficult. In this paper, we consider the problem of automated model repair for adding fault-tolerance where legitimate states are not explicitly given as input. We show that without this input, in some instances, the complexity of model repair increases substantially (from polynomial-time to NP-complete). In spite of this increase, we find that this formulation is relatively complete; i.e., if it was possible to perform model repair with explicit legitimate states, then it is also possible to do so without the explicit identification of the legitimate states. Finally, we show that if the problem of model repair can be solved with explicit legitimate states, then the increased cost of solving it without explicit legitimate states is very small. In summary, the results in this paper identify instances of automated addition of fault-tolerance, where the explicit knowledge of legitimate state is beneficial and where it is not very crucial.
68M15 Reliability, testing and fault tolerance of networks and computer systems
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Sycraft; CUDD
Full Text: DOI
[1] Abujarad, F., Kulkarni, S.: Weakest invariant generation for automated addition of fault-tolerance. Electron. Notes Theor. Comput. Sci. 258(2), 3-15 (2009). Available as Technical Report MSU-CSE-09-29 http://www.cse.msu.edu/cgi-user/web/tech/reports?Year=2009 · Zbl 1294.68048
[2] Alpern, B; Schneider, FB, Defining liveness, Inf. Process. Lett., 21, 181-185, (1985) · Zbl 0575.68030
[3] Alur, R; Henzinger, TA; Kupferman, O, Alternating-time temporal logic, J. ACM, 49, 672-713, (2002) · Zbl 1326.68181
[4] Arora, A; Gouda, MG, Closure and convergence: a foundation of fault-tolerant computing, IEEE Trans. Softw. Eng., 19, 1015-1027, (1993)
[5] Arora, A., Kulkarni, S.S.: Detectors and correctors: a theory of fault-tolerance components. In: International Conference on Distributed Computing Systems (ICDCS), pp. 436-443 (1998) · Zbl 0723.93043
[6] Arora, A., Kulkarni, S.S.: Detectors and correctors: a theory of fault-tolerance components. In: International Conference on Distributed Computing Systems (ICDCS), pp. 436-443 (1998) · Zbl 0817.93003
[7] Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: IFAC Symposium on System Structure and Control, pp. 469-474 (1998)
[8] Avižienis, A; Laprie, J; Randell, B; Landwehr, C, Basic concepts and taxonomy of dependable and secure computing, IEEE Trans. Dependable Secure Comput., 1, 11-33, (2004)
[9] Bang-Jensen, J., Gutin, G.: Digraphs: Theory, Algorithms and Applications, chapter 9, pp. 477-478. Springer, London (2002) · Zbl 1001.05002
[10] Bonakdarpour, B; Ebnenasir, A; Kulkarni, SS, Complexity results in revising UNITY programs, ACM Trans. Auton. Adapt. Syst. (TAAS), 4, 1-28, (2009)
[11] Bonakdarpour, B., Kulkarni, S.S.: Incremental synthesis of fault-tolerant real-time programs. In: International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), LNCS, vol. 4280, pp. 122-136 (2006) · Zbl 1326.68181
[12] Bonakdarpour, B., Kulkarni, S.S.: Exploiting symbolic techniques in automated synthesis of distributed programs with large state space. In: IEEE International Conference on Distributed Computing Systems (ICDCS), pp. 3-10 (2007) · Zbl 0806.68080
[13] Bonakdarpour, B., Kulkarni, S.S.: Masking faults while providing bounded time phased recovery. In: International Symposium on Formal Methods (FM) (2008)
[14] Bonakdarpour, B., Kulkarni, S.S.: Revising distributed UNITY programs is NP-complete. In: Principles of Distributed Systems (OPODIS), pp. 408-427 (2008) · Zbl 0753.68066
[15] Bonakdarpour, B., Kulkarni, S.S.: Sycraft: a tool for synthesizing distributed fault-tolerant programs. In: CONCUR ’08: Proceedings of the 19th International Conference on Concurrency Theory, pp. 167-171. Springer, Berlin, Heidelberg (2008) · Zbl 0753.68066
[16] Bonakdarpour, B; Kulkarni, SS; Abujarad, F, Symbolic synthesis of masking fault-tolerant programs, J. Distrib. Comput. (DC), 25, 83-108, (2012) · Zbl 1285.68016
[17] Bournai, P., Borgne, M.L., Guernic, P.L.: Synthesis of discrete-event controllers based on the signal environment. In: Discrete Event Dynamic System: Theory and Applications, pp. 325-346 (2000) · Zbl 0960.93520
[18] Bouyer, P., Chevalier, F., D’Souza, D.: Fault diagnosis using timed automata. In: Foundations of Software Science and Computation Structure, pp. 219-233 (2005) · Zbl 1118.68374
[19] Bouyer, P., D’Souza, D., Madhusudan, P., Petit, A.: Timed control with partial observability. In: Computer Aided Verification (CAV), pp. 180-192 (2003) · Zbl 1278.68160
[20] Burch, JR; Clarke, EM; McMillan, KL; Dill, DL; Hwang, LJ, Symbolic model checking: 10\(^{20}\) states and beyond, Inf. Comput., 98, 142-170, (1992) · Zbl 0753.68066
[21] Cho, KH; Lim, JT, Synthesis of fault-tolerant supervisor for automated manufacturing systems: a case study on photolithography process, IEEE Trans. Robot. Autom., 14, 348-351, (1998)
[22] D’Souza, D., Madhusudan, P.: Timed control synthesis for external specifications. In: Symposium on Theoretical Aspects of Computer Science (STACS), pp. 571-582 (2002) · Zbl 1054.93502
[23] Ebnenasir, A.: DiConic addition of failsafe fault-tolerance. In: Automated Software Engineering (ASE), pp. 44-53 (2007) · Zbl 1326.68181
[24] Gartner, F, Fundamentals of fault-tolerant distributed computing in asynchronous environments, ACM Comput. Surv. (CSUR), 31, 1-26, (1999)
[25] Gärtner, F.C., Jhumka, A.: Automating the addition of fail-safe fault-tolerance: beyond fusion-closed specifications. In: FORMATS/FTRTFT, pp. 183-198 (2004) · Zbl 1109.68366
[26] Girault, A; Rutten, É, Automating the addition of fault tolerance with discrete controller synthesis, Form. Methods Syst. Des. (FMSD), 35, 190-225, (2009) · Zbl 1186.68051
[27] Gohari, P; Wonham, WM, On the complexity of supervisory control design in the RW framework, IEEE Trans. Syst. Man Cybern., 30, 643-652, (2000)
[28] Henzinger, TA; Nicollin, X; Sifakis, J; Yovine, S, Symbolic model checking for real-time systems, Inf. Comput., 111, 193-244, (1994) · Zbl 0806.68080
[29] Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Computer Aided Verification (CAV), pp. 226-238 (2005) · Zbl 1081.68572
[30] Kulkarni, S.S., Arora, A.: Automating the addition of fault-tolerance. In: Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), pp. 82-93 (2000) · Zbl 0986.68584
[31] Kulkarni, S.S., Ebnenasir, A.: Automated synthesis of multitolerance. In: International Conference on Dependable Systems and Networks (DSN), pp. 209-219 (2004)
[32] Kumar, R; Garg, VK, Optimal supervisory control of discrete event dynamicalsystems, SIAM J. Control Optim., 33, 419-439, (1995) · Zbl 0817.93003
[33] Lin, F; Wonham, WM, Decentralized control and coordination of discrete-event systems with partial observation, IEEE Trans. Autom. Control, 35, 1330-1337, (1990) · Zbl 0723.93043
[34] Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points (extended abstract). In: Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP), pp. 53-66 (1998)
[35] Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: 12th Annual Symposium on Theoretical Aspects of Computer Science (STACS), pp. 229-242 (1995) · Zbl 1379.68227
[36] Mantel, H., C.Gärtner, F.: A case study in the mechanical verification of fault-tolerance. Technical Report TUD-BS-1999-08, Department of Computer Science, University of Technology, Darmstadt (1999) · Zbl 1010.68170
[37] McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Berlin (1993) · Zbl 0784.68004
[38] Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Principles of Programming Languages (POPL), pp. 179-190 (1989) · Zbl 0686.68015
[39] Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: International Colloqium on Automata, Languages, and Programming, Lecture Notes in Computer Science, vol. 372, pp. 652-671. Springer, Berlin (1989) · Zbl 0686.68015
[40] Ramadge, PJ; Wonham, WM, The control of discrete event systems, Proc. IEEE, 77, 81-98, (1989)
[41] Raymond, K, A tree based algorithm for mutual exclusion, ACM Trans. Comput. Syst., 7, 61-77, (1989)
[42] Rudie, K; Wonham, WM, Think globally, act locally: decentralized supervisory control, IEEE Trans. Autom. Control, 37, 1692-1708, (1992) · Zbl 0778.93002
[43] Somenzi, F.: CUDD: Colorado university decision diagram package. http://vlsi.colorado.edu/ fabio/CUDD/cuddIntro.html
[44] Thomas, W.: Handbook of Theoretical Computer Science: Chapter 4, Automata on Infinite Objects. Elsevier Science Publishers B. V., Amsterdam (1990)
[45] Thomas, W.: On the synthesis of strategies in infinite games. In: Theoretical Aspects of Computer Science (STACS), pp. 1-13 (1995) · Zbl 1379.68233
[46] Tripakis, S.: Fault diagnosis for timed automata. In: Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), pp. 205-224 (2002) · Zbl 1278.68140
[47] Tripakis, S., Altisen, K.: On-the-fly controller synthesis for discrete and dense time systems. In: Formal Methods 1999 (FM), pp. 233-252 (1999) · Zbl 1037.93522
[48] Wallmeier, N., Hütten, P., Thomas, W.: Symbolic synthesis of finite-state controllers for request-response specifications. In: Implementation and Application of Automata (CIAA), pp. 11-22 (2003) · Zbl 1279.68221
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.