What
do we want?
In the end, we want to improve the quality of embedded systems. As computer
scientists our focus is on the control part of an embedded system, that can
be either designed or analysed. We always assume that the physical part (the
environment) of an embedded system is given to us. But for the analysis of
the overall system behaviour, of course, both parts, control and environment
in their interaction have to be investigated.
We believe in the power of formal methods and a systematic way of working
when the complexity of systems comes beyond what can be overseen by humans.
Our approach is to derive verification models of embedded systems that are
suitable for computer aided analysis.
Within formal methods, so far, much more effort went into the development
of sophisticated algorithms and tools than into the modelling part. However,
the overall success of the verification approach depends on both, the quality
of the model and the quality of the analysis tools. Here, we want to investigate
how to derive good verification models.
In the context here, modelling requires to split relevant aspects of a system
from irrelevant ones, and formalise the relevant aspects and behaviour. To
be able to do this we need a deep insight in the essence and functioning of
a system. Practice showed that the major contribution to systems validation
comes from systematic modelling. There, typically more bugs are found than
by verification lateron. This makes modelling already a useful task in itself.
In the following we want to discuss our approach and
some basic ingredients. We present the discussion as a list of questions with
answers.
What is a model?
What are good models?
What is the state of the art?
What we do not believe!
What method do we want?
What are the difficulties?
What
is a model?
In our context by model we mean a description of a system
in a formal language. "Blueprint", or simply "description"
could be synonyms that are less overloaded with different meanings. Moreover,
the formal language used should be connectable to a computer aided analysis
tool, eg, in the ideal case be the input language for a model checker of theorem
prover.
What
are good models?
We need models that fulfil some quality criteria. We
identified the following quality criteria that are discussed below:
models
must share the properties of interest with the original system
models
must support computer aided verification
models are transparent
models
must share the properties of interest with the original system
This is the main property of models
in general. It is impossible to explicitly specify in general what the common
properties of original system and model are. For a scale model of a building
or a battle-field model different aspects of what has to be shared between
model and original system are of interest. What is certainly necessary in
our context is that the properties to verify should coincide.
Actually, there is some deeper problem behind this requirement. In essence,
model checking is only a falsification process: a bug found by model checking
can possibly be found back in the original system and, as a consequence, the
original system can be improved. However, in a practical sense this is not
enough. of course, we need also "positive" information about a system.
For example, when solving scheduling problems by model checking, we want to
have that the schedules derived can be used for planning a real process.
models
must support computer aided verification
For one part this means that models must be small; decomposition and
abstraction techniques will therefore play an important role. In this sense
we have a different goal than modelling for software development: there, models
have to be as complete as possible. For another part this means that the modelling
process is also influenced by verification tools available. Good knowledge
of the tools used is unavoidable.
models
are transparent
Here, by transparency we mean that ingredients of the model, ie all the
design decisions are clear and understandable.
What we aim at is a collection of different quality criteria that can be gained
by transparency:
First, we want to have confidence in the "quality" of a model. a
transparent way of model derivation with explicit design decisions can be
useful for justification. Second, modifications in the original problem and
requirements (product families) should lead in an easy, adaptive way to new
models.
The third aspect is model comparison. Often in projects different people work
on the same case study, use different tools, and get different results. A
comparison of the results (and derivation of more general results) is impossible,
when it is not clear to what extent the models are comparable, ie. what design
decisions went into the model.
What
is the state of the art?
"Model hacking preceeds model checking". In most
cases modelling is based on intuition and experience of an expert and design
decisions remain implicit. (we do not want to say that we
want to do modelling without expert knowledge - the contrary is the case.
The point is that decisions are not made explicit, and the models are not
transparent.) We trust a model because we know the person who made the model
(here the point is that there should be other criteria to check the quality
of a model.). In most case studies where models are derived, the focus of
the work is more on demonstration of a certain tool or algorithm, rather than
the modelling aspect, which is one reason for the imbalance between modelling
and verification.
Of course, modelling is a topic in various computer
science and engineering areas. We have to find out what we can learn and transfer
from other areas.
What
we not
do believe:
modelling must
be done by using language XYZ.
modelling must be done by using tool UVW.
modelling is a formal activity.
modelling is an informal activity.
being formally precise right from the beginning gives better models.
a model is always an abstraction of something real.
verification can be done by plugging a model checker to the model of the overall
system design.
We want a method for model derivation with the following steps and ingredients:
Domain specific vocabulary and principles have to be fixed.
Domain specific problem characterists are collected in lists that can be used to support the clarification of the problem statement. They contribute to make the problem statement more transparent. The latter is necessary for adequacy control of the problem statement and for adaption due to problem versions (product families, problem generations). An example of a problem characteristic in the domain of scheduling problems is whether preemption is allowed or not, for programmable logic controllers, whether timing of control and controlled process are in the same range or not, for security protocols whether a communication partner may be known or must be secret. The problem characteristis can be seen as a means to give a problem classification.
Modelling decisions
should be made explicit. Checklists can be useful to select basic, commonly
used principles.
It is necessary to characterise the fragment of the overall problem that is
modelled.
Choices for decomposition have to be made explicit. A discussion on different
ways of decomposition and their consequences can be found here.
One part of principles comes from the problem characteristics, another part
are more generic modelling paradigms. Note, that many modelling decisions
are standard cases, but also the creative element and art of modelling is
hidden here. A process based or architectural based view of a system is not
inherent to the problem itself, it is much more structure added to the original
problem in order to find more easily solutions.
There are modelling
patterns for certain problem characteristics and modelling decisions
available. This allows the re-use of existing solutions and prevents the continuous
re-invention of models. Also, it makes models more transparent and also adaptable.
(We investigate whether Michael Jacksons "problem frames" can be
useful here).
The method is guided by non-monotonic
refinement. Non-monotonic refinement is a process with basically two
ingredients.
The goal is a verification theorem of
the form:
Description_of _the_environment /\ Description_of_the_control
=> System_property
The result of this process is a formal description of the system, here split
in environment and control, and the properties of interest. Note, that the
identification of the relevant system properties is part of the process and
usually not known in the beginning.
Second, we develop this verification theorem in a stepwise manner.
The start is as general and abstract as possible. In each step we add details
based of explicit design decisions and insights. Each design decision applied
can be justified by informal arguments, drawings, engineering blue-prints.
Formally, we add additional assumptions to the left-hand side of our verification
theorem, or natural laws, decompose descriptions, or weaken the properties
that we can prove on the right-hand side of the verification theorem. Patterns,
design decisions, justifications and languages used are certainly domain specific
and it should be useful to offer collections of proved examples to prevent
re-invention of concepts with every new model derived. one kind of design
decisions is based on insight as an an important ingredient in the modelling
process. Look here for a simple example.
Suitable languages must support the process. We consider at least 3 persons that can possibly coincide, the domain expert, the modelling expert and the tool expert. All of them need own languages, but also need common languages. For the own languages we observe the following: first, there must be a language where the domain expert can express domain specific content. Here, every form of documentation of the problem domain should be usable, engineers' drawings, specifications, etc. a second language is necessary for performing the non-monotonic refinement. Third, the tool input is some tool-specific language, and formulating a model in such a language also requires insight in the tool machinery (tool internals) to produce the most efficient models.
What
are the difficulties?
Modelling
has to bridge between an informal original system and a formally described
verification model.
Source for the informality of the original system can be that it is (partly)
a physical system (e.g., a plant), or, that the original system is much to
big to be formally described, or, it contains parts as human users that are
per se not formal. Modelling methods that rely only on informality lack preciseness
and uniqueness: in the end we want to have a formal model with a precise semantics
for verification. Being formally precise allover hides often the essence of
a problem. We observed that with being formally precise we are often more
busy with consistency issues of the formalism used rather than what we intuitively
see as the essence of the problem.
