Building a bridge between Goal-Oriented Requirements with KAOS and event-B System Specifications

Research output: ThesisMaster's Thesis

Abstract

This master thesis presents techniques for connecting requirements models expressed in a goal-oriented requirements engineering (GORE) paradigm into more operational specifications expressed in Event-B. More specifically, the objective was to produce a method that derives an Event-B model from a KAOS model, that relies on the semantics of those two languages, that guarantee a fine-grained traceability and that is as automatic as possible. After reviewing a number of existing approaches, none of those methods seem to answer the problem. Consequently an alternative approach was designed with the central focus of mapping GORE agents to Event-B machines. The work fully relies on the UML-B work for mapping data models. Recent Event-B extensions about machine decomposition are also used to decompose an initial system level machine into more finer grained agent machines based on their ability to control a specific piece of information. Finally the agent machines are refined to match the behaviour declared in the KAOS model. The approach has been partially implemented in a prototype that uses model to model transformation technologies (EMF - ATL), and has been validated on different cases.
LanguageEnglish
QualificationMaster
Supervisors/Advisors
  • Vanhoof, Wim, Supervisor
Publisher
StatePublished - Jun 2010

Fingerprint

Specifications
Requirements engineering
Data structures
Semantics
Decomposition
Electric potential

Keywords

  • Event-B
  • KAOS
  • Requirements Engineering
  • Model-driven Engineering
  • Formal Methods
  • Goal-oriented modelling

Cite this

@phdthesis{0aa122ad9d164c8da7c600ddcbe8bf95,
title = "Building a bridge between Goal-Oriented Requirements with KAOS and event-B System Specifications",
abstract = "This master thesis presents techniques for connecting requirements models expressed in a goal-oriented requirements engineering (GORE) paradigm into more operational specifications expressed in Event-B. More specifically, the objective was to produce a method that derives an Event-B model from a KAOS model, that relies on the semantics of those two languages, that guarantee a fine-grained traceability and that is as automatic as possible. After reviewing a number of existing approaches, none of those methods seem to answer the problem. Consequently an alternative approach was designed with the central focus of mapping GORE agents to Event-B machines. The work fully relies on the UML-B work for mapping data models. Recent Event-B extensions about machine decomposition are also used to decompose an initial system level machine into more finer grained agent machines based on their ability to control a specific piece of information. Finally the agent machines are refined to match the behaviour declared in the KAOS model. The approach has been partially implemented in a prototype that uses model to model transformation technologies (EMF - ATL), and has been validated on different cases.",
keywords = "Event-B, KAOS, Requirements Engineering, Model-driven Engineering, Formal Methods, Goal-oriented modelling",
author = "Xavier Devroey",
year = "2010",
month = "6",
language = "English",
publisher = "Facult{\'e}s Universitaires Notre-Dame de la Paix",

}

Building a bridge between Goal-Oriented Requirements with KAOS and event-B System Specifications. / Devroey, Xavier.

Facultés Universitaires Notre-Dame de la Paix , 2010. 129 p.

Research output: ThesisMaster's Thesis

TY - THES

T1 - Building a bridge between Goal-Oriented Requirements with KAOS and event-B System Specifications

AU - Devroey,Xavier

PY - 2010/6

Y1 - 2010/6

N2 - This master thesis presents techniques for connecting requirements models expressed in a goal-oriented requirements engineering (GORE) paradigm into more operational specifications expressed in Event-B. More specifically, the objective was to produce a method that derives an Event-B model from a KAOS model, that relies on the semantics of those two languages, that guarantee a fine-grained traceability and that is as automatic as possible. After reviewing a number of existing approaches, none of those methods seem to answer the problem. Consequently an alternative approach was designed with the central focus of mapping GORE agents to Event-B machines. The work fully relies on the UML-B work for mapping data models. Recent Event-B extensions about machine decomposition are also used to decompose an initial system level machine into more finer grained agent machines based on their ability to control a specific piece of information. Finally the agent machines are refined to match the behaviour declared in the KAOS model. The approach has been partially implemented in a prototype that uses model to model transformation technologies (EMF - ATL), and has been validated on different cases.

AB - This master thesis presents techniques for connecting requirements models expressed in a goal-oriented requirements engineering (GORE) paradigm into more operational specifications expressed in Event-B. More specifically, the objective was to produce a method that derives an Event-B model from a KAOS model, that relies on the semantics of those two languages, that guarantee a fine-grained traceability and that is as automatic as possible. After reviewing a number of existing approaches, none of those methods seem to answer the problem. Consequently an alternative approach was designed with the central focus of mapping GORE agents to Event-B machines. The work fully relies on the UML-B work for mapping data models. Recent Event-B extensions about machine decomposition are also used to decompose an initial system level machine into more finer grained agent machines based on their ability to control a specific piece of information. Finally the agent machines are refined to match the behaviour declared in the KAOS model. The approach has been partially implemented in a prototype that uses model to model transformation technologies (EMF - ATL), and has been validated on different cases.

KW - Event-B

KW - KAOS

KW - Requirements Engineering

KW - Model-driven Engineering

KW - Formal Methods

KW - Goal-oriented modelling

M3 - Master's Thesis

PB - Facultés Universitaires Notre-Dame de la Paix

ER -