They were tackling the issue of having two or more action systems in parallel; if you refine one of them, do you have a refinement of the whole thing? (monotonicity)
Action systems have no explicit paralleism or processes; these are modelled implicitly by shared memory. For example, if there are no shared variables in a pair of statements then they happen in parallel. Actions are demonically non-deterministic (they always do what you hope they won't).
Action is defined by (p0,A,p) which are initialisation predicate, action and finalisation predicate respectively. Action behaviour is determined by a state sequence where the initialisation predicate and initial state hold. Actions can abort, run to infinity, terminate or be miraculous. The trace of the action is observable, and one removes the unobservable part and finite "stuttering" (where no global variables change).
The main model of the programs is as predicate transformers.
Joakim showed the basic refinement mechanism and extended it to refinement of parallel actions. The trick was, if you had A [= A' and wanted to check that (A||B) [= (A'||B) then you had to check B for non-interference; a guarantee relation [Q] had to hold for actions of B, where Q only needed to constraint global variables.
Given this he split out the action system description from the original 3-tuple to a 7-tuple adding things like an invariant and the guarantee relation. He re-expressed parallel composition and refinement in terms of this new tuple.
Since the abstract information of the component is now public in the tuple, you can show compositionality using several rules which he gave, and also refine both A and B in the above example in different directions while retaining the refinement relation!
There were questions on whether some actions could interfere but
not cause an actual error in refinement, and comparing sequential and
parallel assignment in the action model.
Steve Dunne, U of Teeside
He gave an overview of the various total correctness forms of specification such as:
In all of these, P is a unary predicate over the state space and Q is a binary predicate relating before and after states. He looked at what these meant if P were false, or there was a state in P that was not defined in Q -- this would be a partial (infeasible) state. He summarised the weakest-precondition semantics of Dijkstra+Hoare and the refinement definition in the wp-calculus.
He then pointed out that such predicate pairings aren't in fact a unique canonical form for total correctness specifications, and gave an example of it causing a violation of Leibnitz's law S1 = S2 => S1*S = S2*S for some operator *; Back and Butler identified this defect but Steve doesn't think there's anything worth saying about it.
Steve aims to fix this by normalising the predicate pairs, weakening Q as far as possible without breaking the total correctness meaning. He looked at ways to combine two predicate pairs and introduced his "concert" operator # where [P1,Q1] # [P2,Q2] is such that P1 v P2 |- (P1=>Q1) v (P2=>Q2). It is well-defined and monotonic w.r.t. refinement.
Problem is, anarchic termination can screw this up. He reviewed Ward's work on conjunction and disjunction; Ward had a tamed but non-monotonic version of #. So how to break out of this? A paradigm shift!
"General correctness"; the focus of his research. It's based on the intuition "assuming it terminates then Q holds", using Dijkstra's weakest liberal precondition.
Time was pressing so he outlined the formal semantics of his operator and finished.
He reviewed why people hate testing, which was an excellent technical and social summary of the situation:
He viewed test case generation ans a formal synthesis problem, and proposed to use program synthesis techniques to derive test cases; abstraction as opposed to refinement.
He gave examples of contracts as specifications, using Back+Wright's refinement calculus and incorporating user interaction. His view was that test cases [= spec [= implementation. So how in practice do you make appropriate abstractions?
Mutation testing is a known testing technique; introduce small errors in the source to see if existing test cases can find the error. This gives a selection strategy for test cases based on the hypotheses:
But not all mutations are useful; you may even end up producing a refinement of the specification rather than an abstraction!
A useful mutant of C is a contract Ci such that exists a test case TCi [= C that can distinguish an implementation of Ci from an implementation of C. It is useful iff C [|= Ci. Abstract mutants can be distinguished by testing results which don't match some test case, or with a test input outside the domain.
A test case is defined as adequate with respect to mutation operations M if it can distinguish at least one useful mutant Mi. Bernhard gave an example.
Bernhard defined a rule for mutation testing by expressing relations between contracts, mutants and test cases. Test coverage criteria were defined in terms of refinement, which looked quite neat.
Summary: treat testing as an engineering discipline and prove the quality of your test cases!
Christie reviewed refinement in:
"Data refinement doesn't imply stable failures refinement":
Proof was based on data types P and Q with corresponding processes
ProcP and ProcQ. Christie produced schemas for objects A,B,C with
five distinct states for each and differences in their pre and post
conditions.
P shown to backwards-simulate Q but differ in possible initial states.
She showed what backwards-sim rules needed to be checked and demoed
checking a couple of them. Q then data-refines P.
Looking at ProcP and ProcQ she defined them using action systems. P could non-deterministically be in 1 of 2 states after initialisation so ProcP was correspondingly in a or b. She checked failures of ProcQ, and they weren't a subset of ProcP so there was a mismatch!
The mismatch arose in recording the availability of combinations of operators; the data refinement model doesn't record this. So the simulation (data refinement) rules for Object Z (histories semantic model) are not sound.
She proposed a change to the Object Z backwards-sim rules of reversing forall-exists in one case to exists-forall. The implication was that this was a pretty significant fix though my refinement background wasn't good enough to appreciate the wider implications.
Christie then went on to show a semantic model for CSP corresponding to data-refinement. She noted that the treatment of outputs differed for the CSP failures model; Z has a relational semantics and CSP can't distinguish between output refusal due to unavailability and output refusal because a different output was selected.
If data types A and C communicate then you now need an extra check:
A [R= C <=> process(A) [S= process(C)
which does not generally hold.
You need an additional process identical to the data type except that
the environment can't influence the choice of output value. Given
this, relational refinement of communicating data types == simultaneous
traces refinement of corresponding processes and singleton failures
refinement of corresponding input processes.
In diagrammatic terms, composition is the horizontal process of removing non-determinism from a system by constraining component behaviour; refinement is the vertical process of making the system description more precise.
Uni Lisbon has something called CommUnity; an action-based program design language which supports under-specification and non-determinism. Antonia demonstrated an example model of a bank account with credit facility with constraints about balance, credit amount etc. and another model of a counter which counts how many days a value has been negative since the last time the counter was reset.
The example of superposition extents the account design to monitor the number of days the account was overdrawn by combining the two models above.
Antonia formalised superposition using a morphism beween designs. She noted that you can also use composition morphisms to define system configurations, and applied this by combining a regulator into the model to constrain the account withdrawals.
NB: morphisms don't capture refinement since they don't preserve properties of the required non-determinism during composition. Antonia gave an example of this.
She then defined slightly different morphs where the interval defined by the bounds for enabling conditions of actions must be preserved or strengthened, and showed an example which complied with the limits on the bank account model.
She noted that composition and refinement morphisms are related by a compositional property as specified in the paper [but I couldn't follow the explanation of the relation].
Conclusions:
He summarised Morgan's refinement calculus w.r.t. the notation of variables and noted that in timed refinement one distinguishes input, output and auxiliary variables; in addition there's a distinct variable T (tau) in Time (time domain). [Which is an interesting contrast to my approach which eschews auxiliary variables, and implicitly quantifies conditions over all discrete t].
Notation:
More complex behind the scenes! The timed refinement calculus semantics models local, in and out variables as constant (i.e. defined at system start) functions over the time domain. Specifications introduce T and the "stability" of unchanged variabls implicitly.
The tool programming language includes idle delays and a guarded command language. The refinement laws require certain predicates to be time-insensitive. PRT is built on the Ergo theorem prover, handling proof and refinement steps in the same way. Refinements can be recorded as proof scripts.
Two main kinds of rules during refinement. Transformation refines the current focus, and window open+close rules change the current focus. To implement timed refinement using PRT you need to:
They use the notation E@t to refer to an expression at a specific time.
Colin gave examples of the timed refinement rule "introduce variable" which has lots of provisos on idle-invariance, covering compiler-level concerns such as having to manipulate the stack to get variable space. Note that you can idle forever! But you get around this by using the deadline statement.
A worked example's given in the paper; he noted that the tool does
hide most of the complexity.
Adrian Hilton (and Jon G. Hall), The Open U
I outlined the requirements of emerging standards for safety-related electronic hardware, such as UK Defence Standard 00-54 and IEC 61508. I described the synchronous process algebra SRPT and its proof model. I then extended the algebra with a timed w:[pre,post] specification form and defined refinement rules.
I outlined how I'd refined a width-parametrised carry look-ahead adder from an timed abstract spec into a full implementation. Testing revealed a flaw in the adder due to a manual error in one refinement step, and once the flaw was fixed it worked.
Conclusions: it's a practical process, but has a useful lesson in the need for testing!
Lunch was very enjoyable. I talked with David from Escher Technologies and Helen from Royal Holloway London, both of whom knew of Praxis. David opined that en-route ATC could take humans out of the loop entirely. Having seen some appalling bits of hacked software in my time I disagreed... Susan disagreed too, saying that she'd like to have someone to blame if she got killed in an accident.
I discussed the RHL CompSci courses with Helen. Interestingly their formal methods course is the third most popular optional course. There's hope yet!
My rudimentary Danish proved useful for deciphering the coffee machine instructions before the afternoon's session started.
Why do this?
Note that specifications should not be write-only!
How to do this?
Example: "inline a macro". For all uses of the name:
Not rocket science but when lots of refactorings are composed, each individual step is recheckable along the way. Two main approaches to a process:
To consider proof as refactoring, start with the conjecture to be proven. Proof steps transform a goal to a simpler goal using an inference rule: they are reversible rules which are meaning-preserving and thus can be thought of as refactoring the goal.
Refinement itself is refactoring:
Or (the refinement calculus approach) abstract and concrete specs have the same "essential meaning" so refactor the abstract spec into the concrete one.
When is there the opportunity to refactor? When the spec has:
Refactoring to patterns is one option:
Refactoring tool requirements:
The question for this talk: are there restricted cases where it is safe to replace these operators?
Lindsay defined operator refinement in Z as per the literature, then asked "what if you don;'t have refinement?" Looking at termination or correctness violation.
Monotonicity defined thus: if you substitute a component with a refinement of that component then you get a refinement of the whole. As some Z operators are not monotonic, options are:
Example: conjunction is not monotonic since reducing non-determinism of components can decrease the domain of termination. Lindsay gave examples to back this up. So when is it monotonic?
Let A1, B1 only differ from A,B in having a weaker precondition, i.e. (forall S: A => A') and (forall S: B => B') so A [= pre A1 and B[= pre B1.
There do exist cases where reducing non-determinism doesn't break it -- if A1 and B1 are consistent whenever A, B are then we are OK.
Consistency is defined for A,B on a state S if:
forall S: pre(A) and pre(B) => pre(A and B)
Lindsay pointed out that disjunction isn't monotonic either; problems arise in the opposite manner to conjunction. Increasing termination causes the problems. So what do we need to make it monotonic?
If:
NB: composition isn't monotonic either (not shown in Lindsay's paper). Reducing non-determinism in the first component, A, can decrease the domain of termination. Increasing termination in the second component, B, can increase non-determinism of the whole.
So when is composition monotonic? The conditions are similar to conjunction for the first argument and disjunction for the second argument.
Conclusions:
In this model a program is a sequence of classes plus a main command. There is attribute visibility control, and recursive methods are allowed.
Marcio demonstrated an example of a polygon transform program, which showed the use of class extension (inheritance).
The refactoring rules are based on program compilation to test type errors, and a test suite to find functional errors. Marcio gave the example of the refactor rule "extract method" to pull an extra method out of an existing one. Another example was moving a method from one class to another, and a third example was extracting an entire class.
ROOL rules look like "where <namings> provided <condition>". To derive the correctness of refactor rules Marcio showed the basic laws used and showed several stages of a fairly prolonged derivation.
Conclusions:
Future work is to develop design patterns.
Questions posed by John:
He recapped the definitions made earlier. There are two types of simulation: downward (abstract to concrete) and upward (vice versa). But in Z, specification operations are sometimes partial and so we embed partial relations in the total world. To derive simulation rules in Z we interpret initialisation operations etc. as the appropriate relations. Finalisation makes all outputs visible. John showed an example of the definition for upward simulation in Z.
In failures-divergences (FD) refinement, traces of events are recorded as opposed to I/O relations. John recapped the F,D definitions. So what are the differences?
So how to add refusals to relational refinement? Make more observations by increasing the expressivity of finalisation. John gave a simple Z spec example of a switch. He unwound the downward simulation rule, finding that it places no extra proof obligations on a downward simulation where there is no I/O. For upward simulation, however, this isn't subsumed and so is giving a new proof obligation.
The result of this is that observations have been extended and now record refusals; these appear in the simulation rules. Now when you check vs. FD refinement you can prove correspondence with the blocking and non-blocking models.
Eerke took the baton and described what you needed to do with I/O:
Refusal of an event with an output can be demonic (environment can't influence the choice) or angelic (the environment can influence the output, therefore no refusals are caused due to the particular output chosen). The finalisation must record which approach was used.
Eerke gave the simulation rule for downward and upward simulation in the demonic model, noting that you must look explicitly at what happens with outputs; he justified this with an example.
FD refinement doesn't hold between the systems that he sketched, but upwards simulation without I/O holds. So how to fix?
Look at maximal refusal sets. The finalisation conditions then work, relating maximal refusal sets in the abstract and concrete states.
Eerke summarised the refinement rules for downward and upward simulation. The upward sim gave stronger results than downwards.
Looking at other refinement relations, we can embed other concurrent refinement relations as failure/trace or readiness. If you're doing readiness refinement then you don't know anything about refusals. Note that we can use partial relations directly.
Eerke finished by drawing a diagram summarising the gain made in the simulations and relations by this paper, useful for seeing the big picture.
Circus has refinement laws for actions. A process encapsulates state and reactive actions -- see the FME paper for the details of this.
The case study was a bounded buffer. Jim gave the Z spec for this. Circus adds a channel and process to the specification. The CSP-like syntax describes receipt of an input and the sending of an output. [It's a weird idea but it seems to work pretty well]. Jim was going to work through a non-trivial data refinement, a ring of processes plus a controller to make the ring behave like a circular buffer. The head of the ring was cached in the controller for performance reasons. There was the need for a couple of integer counters to track the head and tail positions and the size of the buffer.
Jim demonstrated refinement of the retrieval relation to cut away the unused ring and shift down until you get to one object. He justified this using a forward simulation.
The state change had two cases: an empty buffer or a non-empty buffer. Again, Jim justified the change decision by forward simulation. Now he was going to try manipulating actions in the CSP part. He had to show that ag & A <= cg & B; (abstract action refined to the concrete action). The guards ag,cg had to be equivalent modulo the retrieval relation.
The use of many processes to replace one process was chosen to illustrate the power of the Circus transforms. It even works for recursive processes, though Jim didn't demonstrate this.
The next decision was how to change the design structure? Decompose the input and output actions, and keep refining until we get the possibility of promotion. He gave an example rule for decomposing a schema into guarded processes, and showed how you do parallel decomposition of input and output actions:
Note that here the blocking/non-blocking semantics debate is kind of irrelevant. Here there are actions to update state and explain reactive behaviour on the state. But there's no 1-1 correspondence between ADT operations and the events that caused them.
Jim proved that the last refinement step was in fact correct. Conclusions:
He quoted the intuition behind refinement: the "principle of substitutivity" (due to Derrick and Bolton). He noted that most literature notions of refinement have restrictive assumptions, e.g. that programs are sequential or that observations are typically pairs of I/O sequences. This makes it hard to look at arbitrary segments of computation that may not produce output. He also outlined other perceived restrictions on the notion of refinement.
Egon's background is as a logician, and he presented an example of a restriction from Abrial's B book: you can't have more than one operation call of a machine at once; it's a violation of the proof principle and breaks the invariant. He contrasted this with the ASM method which allows parallel invocations of submachines, at the price of having to care about correctness proofs.
He showed how ASMs got refinement around 1989. The refinement method is problem-oriented, driven by practical refinement tasks and with the goal of supporting divide+conquer techniques for design and verification.
He noted that to come up with a good refinement you need a good refinement idea and a way to formulate it. Try to exploit reusable proof techniques for system properties. He gave an example of compiler correctness refinement.
Egon noted the gap between hand proof (quick) and machine proof (slow but reliable). He showed how ASM refinement hierarchies used by IBM reused the proof of Prolog->WAM for their CLP(R)->IBM-CLAM proof.
[Around this point the audience were getting restless and/or a bit bolshie...]
To show correctness of a state machine for a notion of equivalence of states, there is a correct refinement iff every (infinite) refined run simulates an (infinite) abstract run with equivalent corresponding states. It is complete iff the refinement is symmetric. Therefore, refinement correctness implies (for terminating runs) equivalence of I/O behaviour.
Egon gave an example of conservative ASM refinement, adding machines incrementally. The example was adding a bytecode verifier to a Java interpreter in the JVM. Procedural refinements corresponded to sequential submachine refinements.
A second example was a debugger control state ASM; (1,1) refinements of ASMs allowed parallelism e.g. Java thread execution.
The aim in ASM refinement is to find commuting diagrams with end points to satisfy an invariant. Egon showed graphical representations with triangles and trapezoids; references were given for further examples.
[It was probably a good thing that this talk was late in the afternoon of
a long day -- if the audience had had a bit more energy, half-bricks might
have been thrown during some of Egon's more controversial statements.]
Asuman Sünbül (and Matthias Anlauff), Kestrel Institute
The existing approach to component-based systems tackles problems at the technology layer and solves the technical component interaction issues. But there are many platforms where these techniques fail, such as massive node collections -- NEST, in this particular case.
Each NEST node ("mote") has its own processor, I/O, memory etc. Cost to build is around $30, and they run off 2xAA batteries. Designers need to optimise code and be careful with the power-draining computation and comms usage. It uses radio waves for communication. Typical uses for motes are as distributed detectors e.g. earthquakes, forest fires. The idea was to throw out all the technical features that weren't needed.
There is the need for a specific architecture to the NEST requirements; a flexible way of representing semantic information about components.
Asuman uses abstract consistency predicates to "fix" a view of the abstract model. "Abstract connectors" connect components without nailing down what they are.
"CMIL" is the Component Model Input Language. It is used to specify systems of components, connectors and their refinement relations. Asuman gave the example of checking connector consistency in a system. She showed an overview of the CMIL checker architecture.
Conclusions:
For the evening meal we rendezvoused at the Cab-Inn Scandinavia then wandered down to Wonderful Copenhagen to meet the town-centre hotel dwellers. There was some discussion about where to eat before Steve Dunne took charge and led us through the station to a Pakistani restaurant at the edge of the red light district.
Twelve of us squeezed around a table and ordered a mix of dishes and a clutch of bevvies, then sat back to enjoy the evening. Talk ranged from viva experiences to books (SS has 15m of unread books on her shelves) to the whole Swedish-English-Finnish thing in Finnish universities to... well, you get the idea.
I sought an inside track on vivas, and got many useful tips. SS threatened to volunteer as my external, which would be wonderful from the point of view of having an examiner who was current with all three fields of my research, and pretty terrifying by any other criterion.
We went for a post-prandial stroll which started in the red light district. It was highly amusing to see a distinguised academic idly looking in a shop window only to slowly realise the extremely anatomical nature of what he was actually seeing. We headed up the east side of the island to Nyhaven. The evening was very pleasant, cool without being cold, and the Danes were out on bikes or strolling down the sidewalks. About 80% of the cyclists were women, go figure.
Finally we headed back along Stroget and split up to go back to our regular hotels. I wasn't back until half eleven, looking forward not at all to another early morning,.