|
The properties of a realistic artefact usually are a compromise between what one wanted ideally and what one was able to realise. Often, one did not even really understand what one wanted. Often, one did not fully understand what was possible. →specifications and →blueprints often did not accompany the developent process. Sometimes preliminary realisations – "rapid prototypes" – were adapted until the developer intuitively felt that the design was correct. If for such a system a correctness theorem were provable, it will first have to be discovered.
Unlike in Monotonic Refinement, the decisions taken in such a chaotic development process are not limited to design decisions . Many decisions are adaptations of the original requirement.
The quality of such a realistic development process can be improved if the seemingly chaotic process is guided by the canonical form of the Correctness Theorem. And if it has not been guided by it, it can be re-engineerd as if it were. This helps...
- to choose the right abstractions for a formal model that can be used for verification,
- to define the boundary between the artefact and its environment,
- to find a meaningful →decomposition,
- not to mix up levels,
- to take design decisions not before they are really understood,
- to define interfaces when it is understood why they are necessary rather than in the beginning of the process,
- to document all decisions in a logical place,
- to understand the impact of design decisions on the overall properties.
What we want to have in the end is a →model satisfying the quality criteria for models: truthfulness,compactness, understandability and tracability.
Introduction
The method starts from a vague idea about desired properties and derives a realisable blueprint together with a realistic specification. The method can be used in these cases:
- There is an idea around desired properties, but no artefact is known that has these properties. In this case the main result will be a blueprint of a new artefact.
- We have an artefact without blueprint and some idea what its intended properties are (→reverse engineering). In this case the main result will be a specification of the artefact.
- We have an incomplete artefact (for example a plant without control program) and an idea of the desired properties. In this case the main result will be a specification of the missing part.
We will use predicate logic as a specification and blueprint language. The disadvantage that specifications are cumbersome to write and read is compensated by the advantage that we can see the essence and that we do not have to fix things like mathematical spaces, interfaces, etc. before we understand them.
Goal
For a given, more or less vague idea of the purpose or desired properties of a not necessarily existing artefact, find:
- a formula A⇒C where C is an acceptable specification of the goal and A a set of acceptable assumptions about the environment,
- a finite, hopefully small number of formal specifications ai⇒ci for each of which a realisation can be obtained (viz. a →decomposition in realisable parts),
- a formalisation N of some domain properties of the environment,
- such that N ∧ (∀ i. ai⇒ci) ⇒ (A⇒C) can be proved.
The method
The theoretical foundation, explanation and examples can be found in System Design as a Creative Mathematical Activity (Mader, Wupper). Here a summary of the method, instantiated for case 3, where the specification of the control for an existing plant has to be derived.
|
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 ai→ci.
- 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 ai and ci 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 systems 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=(a1→c1, a2→c2, ... , an→cn) 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 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=(a1→c1, a2→c2, ... , an→cn) together with S in a systematic way, where the a1→c1 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 C0 - 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 a1→c1 that contributes to C0 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 C0.
- Obtain knowledge about the quantities the component requires and can handle; incorporate these in a1→c1.
- 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 c1 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 a1 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 c1 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 C0 by a weaker A1→C1 that reflects the new state of knowledge.
- A1 will require a certain amount of electricity and detergent as well as drains. C1 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 a1→c1 and A1→C1. Specify it in the same way as a2→c2.
- For example, we will find a heater that provides warm water provided it gets cold water and a certain amount of electrical energy.
- Adapt A1→C1 accordingly, which gives us A2→C2.
- A2 is stronger than A1: cold water and more electricity is required. C2, however, is weaker: even more time is taken.
- Continue this method, adding new processes and their system components until you arrive at a provable
a1→c1, a2→c2, ... , an→cn |= An→Cn
- 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 ai of all processes so that they inlude the settings of the necessary valves and switches, giving a*i.
- 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, An→Cn can no longer be proved. This is where the control program comes in:
- Find a specification X such that
a*1→c1, a*2→c2, ... , a*n→cn, X |= An→Cn
This can be difficult, but brings us into a well-understood problem area: scheduling. The solution may require further weakening of An→Cn, as the overall process takes more time because sub-processes cannot be executed in parallel.
|
Example
Here nearly trivial example for a formula that occurs and is non-monotonically adapted during the method.
Assume that a part–let us call it Sf–in the system under development has to compute a function f. The first version of the specification of the behaviour of that part is:
DEF Sf := ∀t: TIME. ∀v:ℜ. o(t, input, v) ⇒ o(t, output, f(v))
Here, input and output are the interface points of that part. Predicate o states that at a certain moment (here: t) at a certain interface point a certain value occurs and can be observed. When we want to implement this part as a computer with a program using the machine arithmetic, this part can only handle input in the range [minreal..maxreal]. The result will be inaccurate. The computer will sample its input with a period δ. So we cannot really implement specification Sf. We can only implement something like:
DEF Pf := ∀t: N*δ. ∀v:[minreal..maxreal]. o(t, input, v) ⇒ (∃g:[f(v)-ε..f(v)+ε]. o(t+δ, output, g))
If Pf occurs at the left hand side of a Correctness Theorem we will have to weaken the right hand side correspondingly.
This example shows that the ideal part Sf and the realistic part Pf differ in three respects:
- Computations consume time.
- In this case, the output occurs δ seconds too late w.r.t. the ideal specification Sf.
- Computations are not precise in time and value.
- In this case, the input can be δ seconds too old and the arithmetic introduces an error of ε.
- A physical part can never handle arbitrary, unbounded quantities.
- In this case, the domain is [minreal..maxreal]. This is not imited to computers! The same problem would occur when we implement a reactor in a chemical plant: it can only contain a certain amount of substance.
The first and second can be neglected under certain circumstances: For simple artefacts without feedback and without computational loops) one can hope to ensure that delays and rounding errors do not accumulate and that control theory ensures that they can indeed be neglected. One could also use a specification formalism (think of interval arthmetic) that keeps track of possible accumulations and gives an error message when the effect can not be neglected.
The third can never be neglected. Every physical object has a limited capacity. There is no artefact that can handle unbounded quantities. So even if we decide to neglect imprecisions, we will end up with a specification like:
DEF Qf := ∀t: TIME. ∀v:[minreal..maxreal]. o(t, input, v) ⇒ o(t, output, f(v))
If this specification occurs on the left hand side of the correctness theorem for an aeroplane, it can turn out that we will have to adapt the right hand side, the overall specification. We may, for example, have to assume that air turbulence is bounded.
Even the best, well designed coffee machine has a tank of limited capacity. I can replace it by a bigger machine or by a whole coffee factory, but that will not remove limitations altogether. So we better learn to treat them correctly.
Due to inherent limitations of physical parts, quantifiers in ideal specifiations will have to be replaced by bounded quantifiers as son as we decide which real part to use in an artefact. These bounds will have repercussions on other parts and on the overall performance.
Every engineer outside computer science knows this. But textbooks and courses on programming and software engineering traditionally ignore this issue and given students the idea that computers can safely be treated as unlimited. (Have we not all written recursive or iterative programs for the computation of factorials? The first how many factorials fit in an INTEGER word? About twenty? Why write a program where a short table would be smaller and much quicker?) When then a rocket explodes because a computer program cannot handle a big value, newspapers write about "programming errors", while the programmers have done their job as taught. Le Lann pointed out that we should better talk of systems engineering errors: the components of a system simply do not "fit", because some have the wrong capacity.
Case studies
This is a link to a report on a case study which follows this method:
|
