Modeling fault-tolerant system behavior

  • Mario Dal Cin
Part of the Advances in Computing Science book series (ACS)


Aerospace and railroad control systems need to ensure the safety of passengers. To prevent financial losses, banking and telecommunication systems must offer high availability. Such safety- and mission-critical systems require high assurance. To this end, several formal methods for specifying and verifying non-functional system properties like timeliness, safety and liveness have been developed (Leveson et al. 1994, Leeb and Lynch 1996, Kirner and Davis 1996, Bruel et al. 1996, Mok et al. 1996). These methods are intended to give system developers and customers greater confidence that the systems satisfy their requirements. A number of these verification methods are based on finite-state representations and have achieved considerable success in practical applications.


Model Check Binary Relation Fault Tolerance Finite State Machine Temporary Error 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Arbib, M. (1967): Tolerance automata. Kybernetika Cislo 3: 223–233MathSciNetMATHGoogle Scholar
  2. Brink, C., Kahl, W., Schmidt, G. (eds.) (1997): Relational Methods in Computer Science (Advances in Computing Science). Springer, Wien New YorkGoogle Scholar
  3. Browne, M.C., Clarke, E.M. and Grumberg O. (1989): Reasoning about networks with many identical finite state processes. Inf. Comput. 81; 13–31MathSciNetCrossRefMATHGoogle Scholar
  4. Bruel, J.M., France, R.B., Benezekri, A., Raynaud, Y. (1996): A real-time specification environment based on Z and graphical object-oriented modeling techniques. In Proceedings of the First IEEE High-Assurance Systems Engineering Workshop HASE 96, Niagara on the Lake. Canada. IEEEGoogle Scholar
  5. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, K.L., Hwang, L.J. (1992): Symbolic model checking: 1020 states and beyond. Inf. Comput. 98, 2: 142–170MathSciNetCrossRefGoogle Scholar
  6. Campos, S., Clarke E., Minea, M. (1996): Analysis of real-time systems using symbolic techniques. In: Hartmeyer and Mandrioli (eds.) (1996): Formal Methods For Real-Time Computing. J. Wiley, New York, pp. 216–235Google Scholar
  7. Dal Cin, M. (1975): Fuzzy-state automata: their stability and fault tolerance. Int. Journ. of Comp. a. Inform. Sciences Vol. 4: 63–80, and: Modification tolerance of fuzzy-state automata. Int. Journ of Comp. a. Inform. Sciences Vol. 4: 81–93CrossRefMATHGoogle Scholar
  8. Dal Cin, M. (1997): Verifying fault-tolerant behavior of state machines. In Proceedings of the Second IEEE High-Assurance Systems Engineering Workshop HASE 97, Bethesda, Maryland. IEEEGoogle Scholar
  9. Dal Cin, M. (1998): Checking modification tolerance. Internal Report 98-2. IMMD3 University of Erlangen-NürnbergGoogle Scholar
  10. Eriksson, H.-E., Penker M. (1998): UML Toolkit. J. Wiley, New YorkGoogle Scholar
  11. Harel, D. (1987): Statecharts: a visual formalism for complex systems. Science of Computer Programming 8: 231–274MathSciNetCrossRefMATHGoogle Scholar
  12. Heitmeyer, C., Mandrioli, D. (eds.) (1996): Formal Methods For Real-Time Computing. J. Wiley, New YorkGoogle Scholar
  13. Janowski, T. (1995): Bisimulation and Fault-Tolerance. PhD thesis, Department of Computer Science, University of WarwickGoogle Scholar
  14. Kirner, T.G., Davis, A.M. (1996): Nonfunctional requirements of real-time systems. In: Advances in Computers Vol. 42, pp. 1–37. Academic Press, New YorkGoogle Scholar
  15. Lamport, L. (1977): Proving the correctness of multiprocess programs. IEEE Trans. Software Engineering SE-3, 2: 125–143MathSciNetCrossRefGoogle Scholar
  16. Laprie, J.-C. (1992): Dependability: Basic Concepts and Terminology. Dependable Computing and Fault-Tolerant Systems Vol. 5, Springer Verlag, Wien New YorkGoogle Scholar
  17. Lee, P.A., Anderson T. (1990): Fault Tolerance, Principles and Practice. Springer Verlag, Wien New YorkMATHGoogle Scholar
  18. Leeb, G., Lynch, N. (1996): Proving safety properties of the steam-boiler problem. In: Formal Methods for Industrial Applications. Springer Lecture Notes in Computer Science 1165, pp. 318–338. Springer Verlag, Berlin Heidelberg NewYorkCrossRefGoogle Scholar
  19. Leveson, N.G., Heimdahl, M., Hildreth H., Rose, J.D. (1994): Requirements specification for process-control systems. IEEE Trans. Software Engineering. SE. 20, 9: 684–706CrossRefGoogle Scholar
  20. McMillan, K.L., (1993): Symbolic Model Checking. Kluwer, Boston Dordrecht LondonCrossRefMATHGoogle Scholar
  21. Mok, A.K., Stuart, D.A., Jahanian, F. (1996): Specification and analysis of real-time systems: modechart language and toolset. In: Heitmeyer and Mandrioli (eds.) (1996): Formal Methods For Real-Time Computing. J. Wiley, New York, pp. 33–53Google Scholar
  22. Perraju, T.S., Rana, S.P., Sarkar, S.P. (1996): Specifying fault tolerance in mission critical systems. In Proceedings of the First IEEE High-Assurance Systems Engineering Workshop HASE 96, Niagara on the Lake, Canada. IEEEGoogle Scholar
  23. Poincare, H. (1958): The Value of Science. Reprinted by DoverGoogle Scholar
  24. Rushby, J. (1996): Reconfiguration and transient recovery in state machine architectures. Proceedings of the IEEE International Symposium on Fault-Tolerant Computing FTCS-26, Sendai, Japan. IEEE, pp. 6–15Google Scholar

Copyright information

© Springer-Verlag Wien 1998

Authors and Affiliations

  • Mario Dal Cin

There are no affiliations available

Personalised recommendations