Abstract
Assurance of high integrity systems based on closed systems is a challenge that becomes difficult to overcome when a classical testing approach is used; in particular the evidence generated from a classical testing approach may not meet the objectives of rigorous standards. This paper presents a new approach for the formal verification of closed systems, in particular commercial off the shelf (COTS) products. The approach brings together the formal language Event-B, mathematical proof theory and the Rodin toolset and provides the mechanism for creating abstract models of closed systems and to then verify these system properties against operational requirements. From an industrial perspective this approach represents a step change in the use and successful integration of closed systems; using formal methods to guarantee their integration and functionality. The outcome of the proof of concept will provide a solution that will increase the level of confidence on complex system of system solutions containing closed systems. Moreover, it will support the production of safety-cases by providing formal proofs of a system’s correctness.
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
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-b. International Journal on Software Tools for Technology Transfer (STTT) 12(6), 447–466 (2010)
Leuschel, M., Butler, M.: Prob: an automated analysis toolset for the b method. International Journal on Software Tools for Technology Transfer (STTT) 10(2), 185–203 (2008)
Leveson, N.G.: Engineering a safer world: Systems thinking applied to safety. MIT Press, MA (2012)
Madeira, H., Some, R.R., Moreira, F., Costa, D., Rennels, D.: Experimental evaluation of a cots system for space applications. In: Proceedings of the International Conference on Dependable Systems and Networks, DSN 2002, pp. 325–330. IEEE (2002)
Menon, C., Hawkins, R., McDermid, J.: Interim standard of best practice on software in the context of ds 00-56 issue 4. SSEI, University of York, Standard of Best Practice (1) (2009)
Snook, C., Butler, M.: Uml-b and event-b: an integration of languages and tools. In: The IASTED International Conference on Software Engineering, SE 2008, February 12-14 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bicknell, B., Reis, J., Butler, M., Colley, J., Snook, C. (2012). A Practical Approach for Closed Systems Formal Verification Using Event-B. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds) Software Engineering and Formal Methods. SEFM 2012. Lecture Notes in Computer Science, vol 7504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33826-7_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-33826-7_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33825-0
Online ISBN: 978-3-642-33826-7
eBook Packages: Computer ScienceComputer Science (R0)