Taxonomy/supplement/Modelling

Uit Werkplaats
Ga naar: navigatie, zoeken



Ich habe hier entfernt was woanders besser steht. Ist der Absatz hier drunter noch nötig? Oder steht das jetzt in Modelling in the contexts of verification and design?
Hanno Wupper.jpg
Hanno WupperTaxonomy Remove this comment when resolved!


The context in which we operate is the derivation of verification models of embedded systems. By verification model of an embedded system we mean a description of an embedded system in a formal language that is suitable to apply tools as model checkers or theorem provers. It is obvious that every property that is proved holds for the model, but not necessarily for the original embedded system. Therefore, the quality of a model is essential for the usefulness of the whole verification approach. We see the quality of a verification model in three criteria:

  1. The model shares the relevant properties with the original system.
  2. The model is small enough to be analysed with computer support (model checkers, theorem provers).
  3. The derivation process is transparent (i.e. tracable and understandable) such that we are convinced that 1) hold.

The last criterium is necessary, because modelling a (partly) physical system cannot be purely formal. Here, modelling always has to bridge between a real and a formal object. Therefore, insight is in the end a central argument for the adequacy of a model.

Discussion on generality in model derivation

background
stepwise, non-monotonic refinement of the Correctness Theorems


: what are the proper names for the correctness theorem? in fact, it is for a long time during derivation more a goal than a theorem. we did already agree on other names, but i forgot these..... - In the rest of this taxonomy it so far is called Correctness Theorem. Sure, it is a goal until it has been found. But if we want to build a car, we call it "the car we want to build" before it is a car. Isn't that the same?
A.M.Taxonomy Remove this comment when resolved!



But I see the point. We need a name for a piece of text which is a first approximation of the goal, but is not yet a theorem. Didn't R.W. suggest "correctness argument"?
Hanno Wupper.jpg
Hanno WupperTaxonomy Remove this comment when resolved!



yes, it was something like "correctness argument". But, to be honest, i do not like this, because we use so many different correctness arguments - the special character of this implication is not reflected in such a general name.
A.M.Taxonomy Remove this comment when resolved!


it is a proposition that in nonmonotonically refined, its structure gives structure to our chain of arguments. In some sense it is an approximation to a verification theorem.


We call it a "verification requirement" now.
J.M.Taxonomy Remove this comment when resolved!


problem
at which point during derivation do we introduce knowledge about the plant?
examples
  1. the batch plant: we do not want to talk about valves in the first specifications. only when we have identified processes, we introduce valves.
  2. the lego plant: there are two transport processes, from the queue to the scanner, and from the scanner to the sorter. because these both transport processes are performed by one single belt, we could combine them in on transport process right at the beginning.

position 1: (the generalistic position)

keep as long as possible as general as possible, only introduce assumptions/facts/details when they are unavoidable for the further development

discussion
  +  does not restrict possible solutions to early
   -  the solution space can be too big
  +  the structure of the derivation is clearer. if we introduce a belt property
      right in the beginning, and then at some later place another belt property,
      etc, assumptions/design decicions get diffused through the whole process.
      to formulate it positively: compactness in the introduction of details gives
      more structure and understandability to the derivation process
  + propositions seem to remain longer valid through the refinement process
   -  it is difficult to do as if you do not know about some facts when you indeed know them.
       this gives the derivation some artificial flavour, whereas one goal of this method is
       to make a natural way of derivation more formal, with all positive side-effects.

position 2: (the pragmatic position)

introduce things that you know in the beginning immediately.

discussion
   + we are typically not constructing the plant, but are confronted with a plant
     given. It is a bit artificial to do as if some real, physical aspects were not
     there, for the lego example, we know simply that there is only one belt,
     and we should not make things unnecessarily complicated/artificially.
   - logical structure of the derivation possibly suffers (see above)
   - adding all the valves (CS1)  right in the beginning does not add anything
     concerning structure, it is ballast that diffuses the adequate approach.

position 3: (experimental position)

restrict early and possibly make in a later, non-monotonic step a generalisation

discussion
    + this allows to prove more properties in an early stage and find errornous
        configurations, i.e. more efficiency
    -  fixing parameters too early narrows the mind in finding other solutions.
       the generalisation step later is here more difficult.


alltogether: we typically switch between all positions, the point is how to find the good balance. what are more points for discussion?

for comparison: the Beweren en Bewijzen approach

Compare the B&B course material under INHOUD > SYSTEEMONTWIKKELING. The "Criteria voor specificatie en ontwerp" might be interesting. Also look at the first two practicum assignments.

In B&B we try to teach first years students systematic use of the Correctness Theorem. They work as follows. They find it difficult, but eventually succeed.

  1. Keep the criteria in mind!
  2. Write an idealised, simple specification as first approximation of what the system should do. Do not introduce unnecessary detail.
  3. Make a list of system components.
  4. Make a list of interface points via which the components interact. Without such interface points it is not possible to say anything meaningful about a component's behaviour. If a valve is such an interface point, is must be introduced now.
  5. There is always a discussion about interface points vs. components. We can see a valve as interface point like in our case studies. But it can also be a little component, consisting of sub-components.
  6. Make a domain model, i.e. a list of atomic predicates corresponding to observations (measurements) at the interface points.
  7. Write idealised, simple specifications of the components in terms of the predicates of that domain model.
  8. Step back and look where more detail has to be introduced.