View Proposal

Proposer
Adrian Turcanu
Title
Using model checking on Event-B models of non-deterministic algorithms
Goal
Description
Event-B is a mathematical modelling language that can be used to model various transitional systems. The aim of the project is to develop a methodology for constructing Event-B models of non-deterministic algorithm, to apply it on several case studies and to investigate these by using the model checked ProB.
Resources
Background
Url
Difficulty Level
Challenging
Ethical Approval
None
Number Of Students
1
Supervisor
Adrian Turcanu
Keywords
Degrees
Back to List