1 Documentation and Tools

• The main document on the Event-B modelling language and methodology is the book of Jean-Raymond Abrial  [1].
• The Rodin platform is available at the following link.
• The list of symbols is useful for typing symbols which will appear as mathematical notations.
• The first chapter on the modelling language Event-B chapter 1 summarizes details on the foundations and on the applications.
• The second chapter on using the modelling language Event-B for developing sequential algorithms chapter 2 with examples.
• The third chapter on using the modelling language Event-B for verifying contracts for sequential algorithms chapter 3 with examples.
• The chapter  [3] (from  [2].) authored by Dominique Cansell and Dominique Méry and entitled The Event-B Modelling Method: Concepts and Case Studies has benne published from lectures notes given in a Summer School and you can use it for getting details from Event-B see the following link.
• Lectures Notes The Modelling Language at the following link.
• Chapter Event-B at the following link.