Thesis Topic Details

Topic ID:
3473
Title:
Fairness for Event-B
Supervisor:
Kai Engelhardt
Research Area:
Formal Methods
Associated Staff
Assessor:
Carroll Morgan
Topic Details
Status:
Active
Type:
R & D
Programs:
SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
COMP2111
Description:
Event-B pretends to deal with concurrent systems yet it lacks one of the main specification mechanisms usually found in languages targeting concurrency: fairness.

An initial treatment of fairness constraint is discussed in but more qork is required. Possible continuations include (a) extending the body of knowledge related to Event-B and fairness by devising POs and proof obligations, (b) demonstrating their suitability for Event-B by treating interesting examples, and (c) building a prototype Rodin plugin to add fairness constraints, POs, and proof rules to deal with e.g. response properties.
Comments:
--
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.