|Conference:||Formal Verification 2015 (click here to see full programme)|
|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.|
|Biography||John 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.