Bachelorprojekt - Softwareteknologi
Project No. 0212:  Evol/Event-B Developments

Aktuelle

Tidligere

Description:

Event-B (www.event-b.org is a tool in which system may be modelled as a (flat) set of conditional atomic actions and verified using an dedicated verification engine.

In a masther thesis project, Event-B has been enhanced with a textual language (Evol) for structuring systems as sequential concurrent processes, resembling the Promela language of the SPIN model checker. This way, traditional concurrency solutions may be formally verified.

In this project, one or more enhancements to the Evol/Event-B system should be investigated and carried out. These could be:

• Modelling and verification experiments
• Integrating Evol into the Eclipse-based Rodin framework for Event-B
• Adding communication to the Evol language

The Evol to Event-B compiler is written in Scala and knowledge of functional programming an compiler techniques may be an advantage.

Prerequisites:

02158 Concurrent Programming 01257 Functional Programming (recommended) 01256 Logical System and Logic Programming (recommended)

Supervisor(s) Hans Henrik Løvengreen

Sidst opdateret: Nov 24, 2017 af Hans Henrik Løvengreen