Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Arbib, M. (1967): Tolerance automata. Kybernetika Cislo 3: 223–233
Brink, C., Kahl, W., Schmidt, G. (eds.) (1997): Relational Methods in Computer Science (Advances in Computing Science). Springer, Wien New York
Browne, M.C., Clarke, E.M. and Grumberg O. (1989): Reasoning about networks with many identical finite state processes. Inf. Comput. 81; 13–31
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. IEEE
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–170
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–235
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–93
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. IEEE
Dal Cin, M. (1998): Checking modification tolerance. Internal Report 98-2. IMMD3 University of Erlangen-Nürnberg
Eriksson, H.-E., Penker M. (1998): UML Toolkit. J. Wiley, New York
Harel, D. (1987): Statecharts: a visual formalism for complex systems. Science of Computer Programming 8: 231–274
Heitmeyer, C., Mandrioli, D. (eds.) (1996): Formal Methods For Real-Time Computing. J. Wiley, New York
Janowski, T. (1995): Bisimulation and Fault-Tolerance. PhD thesis, Department of Computer Science, University of Warwick
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 York
Lamport, L. (1977): Proving the correctness of multiprocess programs. IEEE Trans. Software Engineering SE-3, 2: 125–143
Laprie, J.-C. (1992): Dependability: Basic Concepts and Terminology. Dependable Computing and Fault-Tolerant Systems Vol. 5, Springer Verlag, Wien New York
Lee, P.A., Anderson T. (1990): Fault Tolerance, Principles and Practice. Springer Verlag, Wien New York
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 NewYork
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–706
McMillan, K.L., (1993): Symbolic Model Checking. Kluwer, Boston Dordrecht London
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–53
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. IEEE
Poincare, H. (1958): The Value of Science. Reprinted by Dover
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–15
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Wien
About this chapter
Cite this chapter
Cin, M.D. (1998). Modeling fault-tolerant system behavior. In: Albrecht, R. (eds) Systems: Theory and Practice. Advances in Computing Science. Springer, Vienna. https://doi.org/10.1007/978-3-7091-6451-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-7091-6451-8_10
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-83206-6
Online ISBN: 978-3-7091-6451-8
eBook Packages: Springer Book Archive