Abstract
Transient faults belong to a wide-spread class of faults typical for control systems. These are the faults that only appear for a short period of time and might reappear later. However, even by appearing for a short time, they might cause dangerous system errors. Hence, designing mechanisms for tolerating and recovering from the transient faults is an acute issue, especially in the development of the safety-critical control systems. In this paper we propose formal development of a software-based mechanism for tolerating transient faults in the B Method. The mechanism relies on a specific architecture of the error detection actions called the evaluating tests. These tests are executed (with different frequencies) on the predefined subsets of the analyzed data. Our formal model allows us to formally express and verify the interdependencies between the tests as well as to define the test scheduling. Application of the proposed approach ensures proper damage confinement caused by the transient faults. Our approach aims at the avionics domain by focusing on formal development of the engine Failure Management System. However, the proposed specification and refinement patterns can be applied in the development of control systems in other application domains as well.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Laprie, J.-C.: Dependability: Basic Concepts and Terminology. Springer, Vienna (1991)
Storey, N.: Safety-critical computer systems. Addison-Wesley, Reading (1996)
Johnson, I., Snook, C., Edmunds, A., Butler, M.: Rigorous development of reusable, domain-specific components, for complex applications. In: Proceedings of 3rd International Workshop on Critical Systems Development with UML, Lisbon, pp. 115–129 (2004)
Johnson, I., Snook, C.: Rodin Project Case Study 2: Requirements Specification Document, RODIN Deliverable D4 - Traceable Requirements Document for Case Studies, Section 3, pp. 24–52 (2005)
Bosch, J.: Design and Use of Software Architectures: Adopting and Evolving a Product-Line Approach. Addison-Wesley, Reading (2000)
Abrial, J.-R., The, B.: Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Schneider, S.: The B Method. An introduction, Palgrave (2001)
Atelier, B.: User Manual, Version 3.6, ClearSy, Aix-en-Provence, France (2003)
Snook, C., Poppleton, M., Johnson, I.: The engineering of generic requirements for failure management. In: Proceedings of 11th International Workshop on Requirements Engineering: Foundation for Software Quality, Oporto, pp. 145–160 (2005)
MATISSE Handbook for Correct Systems Construction, EU-project MATISSE: Methodologies and Technologies for Industrial Strength Systems Engineering, IST-199-11345 (2003)
Abrial, J.-R.: Event Driven Sequential Program Construction (2001), available at: http://www.atelierb.societe.com/ressources/articles/seq.pdf
Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)
Laibinis, L., Troubitsyna, E.: Refinement of fault tolerant control systems in B. In: SAFECOMP 2004. LNCS, vol. 219, pp. 254–268. Springer, Heidelberg (2004)
Snook, C., Walden, M.: Use of U2B for specifying B action systems. In: Proceedings of RCS 2002 – International workshop on refinement of critical systems: methods, tools and experience, Grenoble, France (2002)
Rebaudengo, M., Reorda, M.S., Torchiano, M., Violante, M.: A Source-to-Source Compiler for Generating Dependable Software. In: IEEE International Workshop on Source Code Analysis and Manipulation, pp. 33–42 (2001)
Reis, G.A., Chang, J., Vachharajani, N., Rangan, R., August, D.I.: SWIFT: Software Implemented Fault Tolerance. In: Proceedings of the Third International Symposium on Code Generation and Optimization, March 2005, pp. 243–254 (2005)
Oh, N., Mitra, S., McCluskey, E.J.: ED4I: Error Detection by Diverse Data and Duplicated Instructions. IEEE Transactions on Computers 51(2), 180–199 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Ilić, D., Troubitsyna, E., Laibinis, L., Snook, C. (2006). Formal Development of Mechanisms for Tolerating Transient Faults. In: Butler, M., Jones, C.B., Romanovsky, A., Troubitsyna, E. (eds) Rigorous Development of Complex Fault-Tolerant Systems. Lecture Notes in Computer Science, vol 4157. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916246_10
Download citation
DOI: https://doi.org/10.1007/11916246_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48265-9
Online ISBN: 978-3-540-48267-3
eBook Packages: Computer ScienceComputer Science (R0)