Conference:Formal Verification 2015 (click here to see full programme)
Speaker:John Colley
Organisation:University of Southampton
Presentation Title:Formal, Model-based Development and Verification of Hardware, Software and Cyber-Physical Systems
Abstract:Event-B is a proof-based modelling language and method that enables the systematic development of specifications using a formal notion of refinement. The Rodin platform is the Eclipse-based IDE that provides automated support for Event-B model-based development, refinement and mathematical proof. The Event-B formal modelling and verification method and the associated open source Rodin toolset integrates powerful automated proof, model checking and co-simulation capabilities, and has a large user base of more than twenty industrial organisations. This talk shows how a formal model of system requirements can be captured and refined to an implementation level, enabling formal and simulation-based verification, together with test creation and coverage measurement to begin earlier in the design cycle.

  • Simulation-based verification is under strain as complexity increases.
  • Formal modelling provides a traceable and verifiable link between the requirements, specification and the implementation.
  • Formal modelling enables the integration of formal and simulation-based verification techniques for coverage closure.
BiographyJohn Colley has twenty years of experience in the development of EDA tools for simulation, test generation, code coverage and model checking. He is now Involved in the ongoing development of verification and validation methods for high-consequence systems, both formal and simulation based, in the defence , rail and semiconductor sectors.

View the Presentation Material:


Formal Verification 2015 is made possible through the generous support of our sponsors.
Formal Logo 2015