Refinement patterns for rapid development of dependable systems

ABSTRACT

Although, it is widely recognised that formal methods is the single most important technique for building complex dependable systems, formal methods struggle to gain wide acceptance outside their few traditional application areas. In this paper we investigate a method for mechanised transformation of formal models. We argue that, applied to the vast catalogue of architectural and design patterns for dependable systems, this method can greatly contribute to the applicability of formal methods in development of dependable systems. The discussion is supported by a detailed analysis of the Triple Modular Redundancy pattern and a prototype plugin to the RODIN platform which adds the refinement mechanisation support to the Event-B formal framework.

REFERENCES

• 1: Rodin: Rigorous Open Development Environment for Complex Systems. IST FP6 STREP project, http://rodin.cs.ncl.ac.uk/ (Last accessed: 18 June 2007)
• 2: C. Metayer, J.-R. Abrial, L. V., ed.: Rodin Deliverable D7: Event B language. Project IST-511599, School of Computing Science, University of Newcastle (2005)
• 3: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 4: Lyons, R. E., Vanderkulk, W.: The Use of Triple-Modular Redundancy to Improve Computer Reliability. IBM Journal (1962) 200--209
• 5: Iliasov, A.: Finer Plugin to the RODIN Platform. Version 0.0.1. http://www.iliasov.org/ncl.plugin.finer 0.0.1.jar (Last accessed: 18 June 2007)
• 6: Iliasov, A.: Finer Plugin Introduction. http://www.iliasov.org/FinerPlugin.html (Last accessed: 18 June 2007)