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 on safety. 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.

Assignment description: DD2460_Assignment1B_EventB.pdf Download DD2460_Assignment1B_EventB.pdf