×

Design and verification of fault-tolerant components. (English) Zbl 1234.68040

Butler, Michael (ed.) et al., Methods, models and tools for fault tolerance. Berlin: Springer (ISBN 978-3-642-00866-5/pbk). Lecture Notes in Computer Science 5454, 57-84 (2009).
Summary: We present a systematic approach to design and verification of fault-tolerant components with real-time properties as found in embedded systems. A state machine model of the correct component is augmented with internal transitions that represent hypothesized faults. Also, constraints on the occurrence or timing of faults are included in this model. This model of a faulty component is then extended with fault detection and recovery mechanisms, again in the form of state machines. Desired properties of the component are model checked for each of the successive models. The models can be made relatively detailed such that they can serve directly as blueprints for engineering, and yet be amenable to exhaustive verification. The approach is illustrated with a design of a triple modular fault-tolerant system that is a real case we received from our collaborators in the aerospace field. We use UPPAAL to model and check this design. Model checking uses concrete parameters, so we extend the result with parametric analysis using abstractions of the automata in a rigorous verification.
For the entire collection see [Zbl 1160.68001].

MSC:

68M15 Reliability, testing and fault tolerance of networks and computer systems
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Uppaal; Uppaal2k
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M., Lamport, L.: The existence of refinement mapping. Theoretical Computer Science 82(2), 253–284 (1991) · Zbl 0728.68083 · doi:10.1016/0304-3975(91)90224-P
[2] Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[3] Avizienis, A., Laprie, J.-C., Randell, B.: Fundamental Concepts of Dependability. In: Proceedings of the 3rd IEEE Information Survivability Workshop (ISW 2000), pp. 7–12 (2000)
[4] Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004) · Zbl 1105.68350 · doi:10.1007/978-3-540-30080-9_7
[5] Bernardeschi, C., Fantechi, A., Gnesi, S.: Model checking fault tolerant systems. Journal of Software Testing, Verification and Reliability (STVR) 12(4), 251–275 (2002) · Zbl 05446635 · doi:10.1002/stvr.258
[6] Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction. ACM Transations on Programming Languadge and Ststems 16(5), 1512–1542 (1992) · doi:10.1145/186025.186051
[7] Cousot, P., Cousot, R.: On abstraction in software verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 37–56. Springer, Heidelberg (2002) · Zbl 1010.68506 · doi:10.1007/3-540-45657-0_3
[8] Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems (TOPLAS) 19(2), 253–291 (1997) · Zbl 01936052 · doi:10.1145/244795.244800
[9] Devillers, M.C.A., Griffioen, W.O.D., Romijn, J.M.T., Vaandrager, F.W.: Verification of a Leader Election Protocol - Formal Methods Applied to IEEE 1394. Formal Methods in System Design 16(3), 307–320 (2000) · doi:10.1023/A:1008764923992
[10] Gebremichael, B., Vaandrager, F.W., Zhang, M.: Analysis of the Zeroconf Protocol Using UPPAAL. In: Proceedings of the 6th Annual ACM & IEEE Conference on Embedded Software (EMSOFT 2006), pp. 242–251. ACM Press, New York (2006) · doi:10.1145/1176887.1176923
[11] Gnesi, S., Lenzini, G., Martinelli, F.: Logical specification and analysis of fault tolerant systems through partial model checking. In: Proceedings of the International Workshop on Software Verification and Validation (SVV 2003). Electronic Notes in Theoretical Computer Science, vol. 118, pp. 57–70 (2003) · Zbl 1272.68249 · doi:10.1016/j.entcs.2004.09.032
[12] Jensen, H.E.: Abstraction-Based Verification of Distributed Systems. Phd thesis, Department of Computer Science, Aalborg University, Denmark (June 1999)
[13] Jensen, H.E., Larsen, K.G., Skou, A.: Scaling up uppaal. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 19–30. Springer, Heidelberg (2000) · Zbl 0986.68519 · doi:10.1007/3-540-45352-0_4
[14] Johnson, B.W.: Design and analysis of fault-tolerant digital systems. Addison-Wesley Publishing, Reading (1989)
[15] Liu, Z., Joseph, M.: Specification and verification of fault-tolerance timing, and scheduling. ACM Transactions on Programming Languages and Systems 21(1), 46–89 (1999) · doi:10.1145/314602.314605
[16] Liu, Z., Joseph, M.: Verification of fault-tolerance and real time. In: FTCS 1996, pp. 220–229. IEEE Computer Society Press, Los Alamitos (1996)
[17] Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property Preserving Abstractions for the Verification of Concurrent Systems. Formal Methods in System Design 6(1), 11–44 (1995) · Zbl 0829.68053 · doi:10.1007/BF01384313
[18] Schneider, F., Easterbrook, S.M., Callahan, J.R., Holzmann, G.J.: Validating requirements for fault tolerant systems using model checking. In: Proceedings of the 3rd International Conference on Requirements Engineering, pp. 4–13. IEEE Computer Society Press, Los Alamitos (1998)
[19] Simons, D.P.L., Stoelinga, M.: Mechanical verification of the IEEE 1394- a root contention protocol using Uppaal2k. International Journal on Software Tools for Technlogy Transfer, 469–485 (2001) · Zbl 1053.68580
[20] Stoelinga, M.I.A., Vaandrager, F.W.: Root contention in IEEE 1394. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 53–74. Springer, Heidelberg (1999) · doi:10.1007/3-540-48778-6_4
[21] Yorav, K.: Exploiting syntactic structure for automatic verification. PhD thesis, The Technion, Israel Insitute of Technology (2000)
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.