Assignment 1B. Safety-security modelling in Event-B using Rodin platform

The goal of the assignment is to learn how to model safety-critical systems in Event-B and understand the impact of security protection mechanisms as well as model security requirements such as role-based access control . One pdf file should be uploaded. The file should contain the requirements document as well as the created specifications. The snapshot of the proof status should be also included.

A note on the the use of Rodin platform for refinement: you can rightclick on a machine and choose "Refine" in the dropdown menu. A machine which is a copy of current with all the events "Refined" will be created. Similarly, rightclick on a context would allow you to create a context which extends the current.

A note of prover use: some proof obligations can be discharged if you use pp or mc alternatives.

Assignment description:  Assignment Event-B Advanced 2023.pdf Download Assignment Event-B Advanced 2023.pdf