Brontekst bekijken van Taxonomy/supplement/Non-monotonic refinement for embedded systems

After the preliminary choices of a {{*|view}} and the languages and tools to be used for verification, the verification model can be constructed.

=== Methodology ===
The method proposed here is not meant to replace existing methods and tools. Rather, it should be applied in conjunction with the method you like to use. The purpose of our method is 
* to help take decisions not before they are well-understood,
* to draw a clear border between the artefact to be modelled and its environment,
* not to blur the modelling process with details before these become essential,
* to make decisions explicit and to order them systematically,
and thus to break down the arguments used for construction of the verification model into such small and understandable, logically ordered pieces that these together give confidence in the truthfulness of the exercise. 

Our method is not confined to a specific formalism or tool, but is based on the following assumptions:

# The verification languages and tools used ...
## allow to write 
### specifications (formulae or automata diagrams or anything that has well-defined semantics in a mathematical space) stating what is ''known'' about a physical artefact or part of it,
### a specification of the properties to be verified,
## help to prove if the first satisfy the second;
## and moreover allow to distinguish between assumptions and commitments (see below).
# The artefact under discussion has been constructed by binding together certain parts with well-understood properties such that these parts together bring forward the desired overall property - even if it may be difficult to recognise these parts without the help of a domain expert. 
# Each physical part of the artefact is required to perform its task ("commitment") only as long as its environment guarantees certain conditions like temperature, power supply, and the necessary input ("assumption"). If we don't have good reasons to abstract from such assumptions, we write specifications as (assumption, commitment) pairs. The specific notation will depend on the languages used. Below, we shall use the notation  a<sub>i</sub>→c<sub>i</sub>.
# For each physical part, quantitative knowledge is available about the time it needs to perform its task and the quantities of volume, current, voltage etc. it can handle. This means that formulae a<sub>i</sub> and c<sub>i</sub> to be found will contain numbers rather than vague terms like "as soon as possible".

=== Goal ===
Whichever languages, methods and tools are used for formal verification, the essence of the ''formal'' part of verification of {{*|embedded system}}s consists in finding out by means of computer support whether
 P, X |= S
where S=(A→C), the specification of the goal, is a formula defining a desired property of the artefact under discussion, X is a specification of the control program, and P=(a<sub>1</sub>→c<sub>1</sub>, a<sub>2</sub>→c<sub>2</sub>, ... , a<sub>n</sub>→c<sub>n</sub>) is a set of formulae specifying something we know about the physical parts of the artefact that are to be controlled.

A formula, however, cannot directly define a physical phenomenon. The semantics of a formula defines a mathematical object, which hopefully corresponds somehow to the intended physical phenomenon. We reserve the term '''specification''' of a physical phenomenon  for a formula that defines a truthful [[Taxonomy/1._Quality/2._Models|mathematical model]] of that phenomenon. Finding a verification model for an embedded system means finding specifications P, X and S.

Many valuable papers on formal verification start by presenting some P, X and S small and readable enough to be useful. Here, we are interested in the decisions that went into finding them. Together with each step, these should be documented.

# '''S, the specification of the goal''' or of the property to be verified, is the first problem. Essentially, there are three possibilities:
## S is given, for example because the embedded system under discussion is part of a bigger artefact, the design of which ''requires'' S. Example: "Each message sent must arrive after at most 100ms" just because otherwise the surrouding system would fail to work. 
## Only a vague idea around the goal is given ("Produce fresh coffee a.s.a.p."), but the specific implementation determins the quantities ("one cup of 80cc per minute"). In order to formulate a provable S we need knowlegde about implementation choices. The method proposed here intends to extract this knowledge in a systematic way.
## Only a vague idea around the goal is given, but we are content with the verficiation of very general properties (like "Each message must arrive eventually." or "If something is produced, it must be coffee.") Without extra knowledge, such specifications are purely academic, as in practice there is no difference between "eventually" and "not yet, and may be not in the next hundred years". Verification of such a general S, however, can be meaningful in front of a background of exra knowledge, which should always be clearly stated for start. For example: "We have good reasons to assume that, if a message arrives at all, it will arrive soon enough. In this verification problem we only want to focus on construction faults that lead to infinite loops." or "If the machine produces something at all, it will be a cup per minute fair enough. We only want to exclude that soup powder gets into the coffee due to a control fault."
# '''P, the specification of the plant, machine, or vehicle in which the control is embedded''', is a much bigger problem. The physical artefact is much too complex that we could attempt to model it completely. We have to construct a truthful model that is small enough to handle, and we have nothing but the physical artefact, some informal diagrams and descriptions and, in the best case, domain experts that are willing to help with their nowlegde. Our method aims at deriving P=(a<sub>1</sub>→c<sub>1</sub>, a<sub>2</sub>→c<sub>2</sub>, ... , a<sub>n</sub>→c<sub>n</sub>) together with S in a systematic way, where the a<sub>1</sub>→c<sub>1</sub> are (hopefully simple) assumptions and commitments for a (hopefully small) number of constituing parts of the artefact. (Example: A mechanical wrist watch should not be seen as lots of tooth wheels, springs and other strange contraptions; it should be understood to consist of an oscillator with frequency 5 Hz, a source of mechanical energy, three hands, and a mechanism to bring the frequency of an oscillator down to 1/(60*5), 1/(60*60*5), and 1/(12*60*60*) of its value, respectively.)
# '''X, the specification of the control program''', can then be understood as the unknown variable in P, X |= S. If the control program already exists, it is tempting to use it - or rather its denotational semantics - as its own specification. But verification of a large program w.r.t. P and S will usually be far too complex for contemporary tools. If X is the weakest specification sufficient to ensure P, X |= S we can first prove this and then verify the program against its specification X independently of its environment: the well-understood question of program correctness.
=== The method ===
This is the method step by step. We will use a washing machine as running example. We hope that the reader sees how the informal specifications we suggest can be formalised in her favourite language.

; Start from C<sup>0</sup> - a simple, general version of the property to be verified.
: A formula (depending on the language used) that says: "Clean clothes, at any time, immediately!". We know that we mean "as soon as possible", but that will not be expressible in most specification languages.
; Use expert knowledge about the artefact to identify a sub-process that somehow contributes to this goal.
: An obvious choice is: move the clothes in warm water with a detergent.
; For that process, find a component in the physical artefact that is used to perform it.
: In our example, this will be a tumbler together with its engine.
; For this component, write a formula a<sub>1</sub>→c<sub>1</sub> that contributes to C<sup>0</sup> but does not contain more knowledge than necessary to contribute to the overall goal.
: If clothes, warm water and a detergent are in the tumbler in the beginning, and if the engine is powered for a certain period, the clothes will be rather clean - and wet - in the end. At this moment we may realise that we forgot to require sufficiently ''dry'' clean clothes in C<sup>0</sup>.
; Obtain knowledge about the quantities the component requires and can handle; incorporate these in a<sub>1</sub>→c<sub>1</sub>.
: This is the moment to decide whether we are modelling a household washing machine or a professional one. In casu, no more clothes than 4.5 kg can be handled, and the process will require 30l of water of 60C and last one hour if it has to remove 99% of the dirt. The c<sub>1</sub> will also tell us that there is a lot of dirty water te be disposed of, and that the clothes are wet.
; Decide what of the a<sub>1</sub> will be ensured by another component of the artefact and what has to be provided by the environment of that artefact.
: In our example the warm water will be provided by a built-in heater, while electricity and detergent will have to be provided by the environment.
; Decide what of the c<sub>1</sub> will have to be dealt with by another component.
: As we want rather dry clothes, we need some kind of spin-dryer and a pump. The necessary drain we shall require form the envorinment.
; Replace C<sup>0</sup> by a weaker A<sup>1</sup>→C<sup>1</sup> that reflects the new state of knowledge.
: A<sup>1</sup> will require a certain amount of electricity and detergent as well as drains. C<sup>1</sup> will contain the quantities 4.5 kg, 1 hour, and 99%. 
; Now look at one of the processes that were discovered during the previous step to decrease the "difference" between a<sub>1</sub>→c<sub>1</sub> and A<sup>1</sup>→C<sup>1</sup>. Specify it in the same way as a<sub>2</sub>→c<sub>2</sub>.
: For example, we will find a heater that provides warm water provided it gets cold water and a certain amount of electrical energy.
; Adapt A<sup>1</sup>→C<sup>1</sup> accordingly, which gives us A<sup>2</sup>→C<sup>2</sup>.
: A<sup>2</sup> is stronger than A<sup>1</sup>: cold water and more electricity is required. C<sup>2</sup>, however, is weaker: even more time is taken.
; Continue this method, adding new processes and their system components until you arrive at a provable:
 a<sub>1</sub>→c<sub>1</sub>, a<sub>2</sub>→c<sub>2</sub>, ... , a<sub>n</sub>→c<sub>n</sub> |= A<sup>n</sup>→C<sup>n</sup>
: In our example, only a pump has to be added. The tumbler, together with its engine powered with a higher voltage and with the pump will do the job.

Not before we have obtained this complete picture, we start with the difficult part of conflicting resources. The specification of one of the processes in our example requires that the water stays in the tumbler for a certain period, while the specification of another one requires it to be pumped out while no new water streams in. A physical tumbler cannot implement both specifications unless it has valves that can be opened and closed. Likewise, engines and pumps must have switches to activate and deactivate them.

; Adapt the a<sub>i</sub> of all processes so that they inlude the settings of the necessary valves and switches, giving a*<sub>i</sub>.
: The process pumping the water out of the tumbler, for example, will require the tap to be closed, the drain to be pened and the pump to be switched on.

From these adapted specifications, A<sup>n</sup>→C<sup>n</sup> can no longer be proved. This is where the control program comes in:

; Find a specification X such that
 a*<sub>1</sub>→c<sub>1</sub>, a*<sub>2</sub>→c<sub>2</sub>, ... , a*<sub>n</sub>→c<sub>n</sub>, X |= A<sup>n</sup>→C<sup>n</sup>

This can be difficult, but brings us into a well-understood problem area: scheduling. The solution may require further weakening of A<sup>n</sup>→C<sup>n</sup>, as the overall process takes more time because sub-processes cannot be executed in parallel.