Synthesis of Event-Based Controllers for Software Engineering
Author(s)
D'Ippolito, Nicolas
Type
Thesis
Abstract
Behavioural modelling has been widely used to aid in the design of concurrent
systems. Behaviour models have shown to be useful to uncover design
errors in early stages of the development process. However, building correct
behaviour models is costly and requires significant experience. Controller
synthesis offers a way to build models that are correct by construction. Existing
software engineering techniques for synthesising controllers have various
limitations. Such limitations can be seen as restrictions in the expressiveness
of the controller goals and environment model, or in the relation between
the controllable and monitored actions. The main aim of this thesis is the
development of novel techniques overcoming known limitations of previous
approaches and methodological guidelines for synthesising useful controllers.
This thesis establishes the framework for controller synthesis techniques that
support event-based models, expressive goal specifications, distinguish controllable
from monitored actions and guarantee achievement of the desired
goals. Together with these techniques, methodological guidelines are proposed
to help in building more accurate descriptions of the environment and
more effective controllers.
In addition, this thesis presents a tool that implements the proposed techniques.
Evaluation of the techniques has been conducted using the tool
to model known case studies from the literature, showing that by allowing
more expressive controller goals and environment models, and explicitly distinguishing
controllable and monitored actions such case studies can be more
accurately modelled and solutions guaranteeing satisfaction of the goals can
be achieved.
systems. Behaviour models have shown to be useful to uncover design
errors in early stages of the development process. However, building correct
behaviour models is costly and requires significant experience. Controller
synthesis offers a way to build models that are correct by construction. Existing
software engineering techniques for synthesising controllers have various
limitations. Such limitations can be seen as restrictions in the expressiveness
of the controller goals and environment model, or in the relation between
the controllable and monitored actions. The main aim of this thesis is the
development of novel techniques overcoming known limitations of previous
approaches and methodological guidelines for synthesising useful controllers.
This thesis establishes the framework for controller synthesis techniques that
support event-based models, expressive goal specifications, distinguish controllable
from monitored actions and guarantee achievement of the desired
goals. Together with these techniques, methodological guidelines are proposed
to help in building more accurate descriptions of the environment and
more effective controllers.
In addition, this thesis presents a tool that implements the proposed techniques.
Evaluation of the techniques has been conducted using the tool
to model known case studies from the literature, showing that by allowing
more expressive controller goals and environment models, and explicitly distinguishing
controllable and monitored actions such case studies can be more
accurately modelled and solutions guaranteeing satisfaction of the goals can
be achieved.
Date Issued
2013-01
Date Awarded
2013-07
Copyright Statement
Attribution NoDerivatives 4.0 International Licence (CC BY-ND)
Advisor
Piterman, Nir
Uchitel, Sebastian
Publisher Department
Computing
Publisher Institution
Imperial College London
Qualification Level
Doctoral
Qualification Name
Doctor of Philosophy (PhD)