[10-28]Software and System developments using Formal Models, Refinements, and Proofs with Event-B
Date:2011-10-08
Title: Software and System developments using Formal Models, Refinements, and Proofs with Event-B
Speaker: Prof. Jean-Raymond Abrial (ETH, Swiss)
Time: 3:00pm, Oct. 28th (Friday), 2011
Venue: Lecture Room, 3rd Floor, Building No. 5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract:
Formal Models construction is the prerequisite approach we take before embarking into programming and, more generally, system development. Our approach can be compared to that of UML. However, formal modeling with Event-B has a very solid semantical basis.
Refinement is the process by which system and software models are constructed using a series of more and more accurate steps taking account of more and more functionalities of the system we want to build.
Proving is the approach we adopt here in order to verify our models. It is done with a tool, the Rodin Platform, that generates what is to be proved and help the user proving these generated statements, mostly automatically but also interactively.
The overall approach is called Event-B.
The presentation contains a quick introduction to Event-B together with an illustrating example focusing on the main topics of an Event-B development: requirements, refinement strategy, refinement, and proofs. The example will be illustrated by a demo on the Rodin Platform.
Bio:
Jean-Raymond Abrial is the co-inventor of Z, B and Event-B. He is the author of the “B-book” (CUP 1996), which presents the B-Method. He published recently a new book \Modeling in Event-B: System and Software Engineering" (CUP 2010). He was a guest Professor at ETH Zurich from 2004 to 2007 where he led the team developing the Rodin Platform for Event-B (funded by the European Project Rodin). After that, he was a researcher also at ETH Zurich, working on a new European Project called Deploy till May 2009. Before being in Zurich, he was a consultant for more than 20 years working in close contact with industrial companies but also with various universities around the world.