Model Driven Development of Data Sensitive Systems

Model-driven development strives to use formal artifacts during the development
process. Formal artifacts enables automatic analyses of some aspects of the
system under development. This serves to increase the understanding of the
(intended) behavior of the system as well as increasing error detection and
pushing error detection to earlier stages of development.

The complexity of modeling and the size of systems which can be analyzed
is severely limited when introducing data variables. The state space grows
exponentially in the number of variable and the domain size of the variables.
This quickly leads to state-space explosion problems and usually results in data
being abstracted away in the models. This works great for systems where the
particular values of the variables do not significantly alter the execution of the
system. Examples of this type of system are transport protocols or pure storage
systems, where the actual values of the data is not relevant for the behavior of
the system. For many systems the values are important. For instance the control
flow of the system can be dependent on the input values. We call this type of
system data sensitive, as the execution is sensitive to the values of variables.

This theses strives to improve model-driven development of such data-sensitive
systems. This is done by addressing three research questions. In the first
we combine state-based modeling and abstract interpretation, in order to ease
modeling of data-sensitive systems, while allowing efficient model-checking and
model-based testing. In the second we develop automatic abstraction learning
used together with model learning, in order to allow fully automatic learning
of data-sensitive systems to allow learning of larger systems. In the third we
develop an approach for modeling and model-based testing of stateless systems
with very large input and output domains.