Event-B is concerned with formalizing specifications. Formal models allow us to perform a more rigorous analysis of our system (thereby improving the quality) and allows us to reuse the specification in the development of an implementation. This comes at the cost of higher up-front investments. This differs from the traditional development process. In a formal development, we transfer some effort from the test phase (where the implementation is verified) to the specification phase (where the specification in relation to the requirements is verified).

Start by watching this Video: In this episode of Verification Corner, Jean-Raymond Abrial and Rustan Leino (Microsoft) show how to do a design starting from a model that is gradually refined toward executable code. They use the Rodin tool, which supports the Event-B formalism.

• JRA Lecture 1: Intro

• JRA Lecture 2: Bridge Controller

• JRA Lecture 3; Mechanical Press

• JRA Lecture4: Sequential Programs

• JRA and Rustan Leino: Hypervisor

• Main Event-B website
• Rodin Download Site (Rodin 3.2). We also install the latest Atelier B provers, the SMT Solvers, ProB, and EventB to Latex plugins. You may want to use Rodin on the Prism workstations or the SEL Virtual Machine which has all these parts as well as Latex.
• Event-B Language and Slides
• Rodin 3.1 Release notes. Rodin 3.2 release notes
• Rodin Manual v2.8

Rodin is available on the Prism Workstations and the SEL Virtual Machine (which also included an install of Latex).

1. Download Rodin for your platform and install.

2. Install the Atelier B provers.Please proceed as follow: From the main menu bar, select Help > Install New Software…. The Install wizard opens. Uncheck the Contact all update sites during install to find required software check box. Click on the Work with dropdown list and select the Atelier B provers update site. Select Atelier B provers in the list (tick the left check boxes) and click Next After some time, the Install window opens. Just click Next, and accept the terms in the license agreement. Click Finish. The update manager downloads the Atelier B Provers feature. Finally, in the next window, click Yes to restart the platform. Plugins.

3. Install ProB and AnimB

4. Install B2Latex. In the install new plugins it is found under: Rodin - http://rodin-b-sharp.sourceforge.net/updates

5. Install SMT Solvers

• Generated Proof obligations

• Department of CSE Home Page
• York Exam Schedule