Software and System developments using Formal Models, Refinements, and Proofs with Event-B

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.

The bio of the speaker is attached below.