2012 | OriginalPaper | Buchkapitel
A Practical Approach for Closed Systems Formal Verification Using Event-B
verfasst von : Brett Bicknell, Jose Reis, Michael Butler, John Colley, Colin Snook
Erschienen in: Software Engineering and Formal Methods
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.