Behavioural Preservation in Fault Tolerant Patterns

  • Diego Machado Dias
  • Juliano Manabu Iyoda
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7021)


In the development of critical systems it is common practice to make use of redundancy in order to achieve higher levels of reliability. There are well established design patterns that introduce redundancy and that are widely documented and adopted by the industry. However there have been few attempts to formally verify some of them. In this work we modelled three fault tolerant patterns (homogeneous redundancy, heterogeneous redundancy and triple modular redundancy) using the HOL4 theorem prover in order to prove that the application of these patterns preserves the behaviour of the original system. Our model takes into account that the original system (without redundancy) computes a certain function with some delay and is amenable to random failure. We illustrate our approach with a case study that verifies in HOL4 that a fault tolerant design applied to a simplified avionic elevator system does not introduce functional errors. This work has been done in collaboration with the Brazilian aircraft manufacturer Embraer.


Redundancy management fault tolerance behavioural preservation theorem proving HOL 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
  2. 2.
    Armoush, A.: Design Patterns for Safety-Critical Embedded Systems. Dissertation, Embedded Software Laboratory - RWTH Aachen University (June 2010)Google Scholar
  3. 3.
    Bremond-Gregoire, P., Lee, I., Gerber, R.: ACSR: An algebra of communicating shared resources with dense time and priorities. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 417–431. Springer, Heidelberg (1993)Google Scholar
  4. 4.
    Butler, R.W., Di Vito, B.L., Holloway, C.M.: Formal design and verification of a reliable computing platform for real-time control (phase 3 results). Technical memorandum 109140 (1994)Google Scholar
  5. 5.
    Camilleri, A., Gordon, M., Melham, T.: Hardware verification using higher-order logic. In: Borrione, D. (ed.) Proceedings of the IFIP WG 10.2 Working Conference on From HDL Descriptions to Guaranteed Correct Circuit Designs, pp. 43–67. North-Holland (1987)Google Scholar
  6. 6.
    Church, A.: A simple theory of types. Journal of Symbolic Logic 5, 56–68 (1940)CrossRefzbMATHGoogle Scholar
  7. 7.
    Dajani-Brown, S., Cofer, D.D., Bouali, A.: Formal Verification of an Avionics Sensor Voter Using SCADE. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 5–20. Springer, Heidelberg (2004)Google Scholar
  8. 8.
    Douglass, B.P.: Real-Time Design Patterns: Robust Scalable Architecture for Real-Time Systems. Addison-Wesley Professional (2002)Google Scholar
  9. 9.
    Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press (1993)Google Scholar
  10. 10.
    Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language Lustre. Proceedings of the IEEE 79(9), 1305–1320 (1991)CrossRefGoogle Scholar
  11. 11.
    The HOL4 System. SourceForge website,
  12. 12.
    International Electrotechnical Commission. IEC 61131-3 Ed. 1.0 en:1993: Programmable controllers — Part 3: Programming languagesGoogle Scholar
  13. 13.
    Keith, L.: Advisory Circular - System Design and Analysis, 25.1309-1A (June 1988)Google Scholar
  14. 14.
    Koren, I., Krishna, C.M.: Fault Tolerant Systems. Morgan Kaufmann Publishers Inc., San Francisco (2007)zbMATHGoogle Scholar
  15. 15.
    Melliar-Smith, P.M., Rushby, J.: The Enhanced HDM system for specification and verification. In: VerkShop III, Watsonville, CA, pp. 41–43 (1985)Google Scholar
  16. 16.
    Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification of fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering 21(2), 107–125 (1995)CrossRefGoogle Scholar
  17. 17.
    Sokolsky, O., Lee, I., Ben-Abdallah, H.: Specification and analysis of real-time systems with PARAGON (1999)Google Scholar
  18. 18.
    Sokolsky, O., Younis, M.F., Lee, I., Kwak, H.-H., Zhou, J.X.: Verification of the redundancy management system for space launch vehicle: A case study. In: IEEE Real Time Technology and Applications Symposium, pp. 220–229 (1998)Google Scholar
  19. 19.
    Melham, T.F.: Abstraction mechanisms for hardware verification. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) VLSI Specification, Verification, and Synthesis, pp. 129–157. Kluwer Academic Publishers, Boston (1988)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Diego Machado Dias
    • 1
  • Juliano Manabu Iyoda
    • 1
  1. 1.Centro de InformáticaUniversidade Federal de PernambucoRecifeBrazil

Personalised recommendations