Another pleasant breakfast. There's something inherently right about eating cold meat for breakfast. Buoyed by protein and caffeine I got off the number three bus one stop early by mistake, but walked up a block and got the 185 anyway.
The steps in the development of his calculus were:
The biggest problem they have is that they still don't have a tool to support this work.
A knowledge-based program is in the style of a guarded command program
with additional tests for knowledge.
if !K1.K2 bit then send(1->2)(bit)
== "if agent 1 does not know that agent 2 knows the bit's value then send
bit from agent 1 to agent 2".
A potential implementation for a lossy channel, for instance:
if !received(1<-2)(ack) then send(1->2)(bit)
The semantics of knowledge are as follows:
He set out criteria for an agent knowing p. To evaluate a knowledge test you need a system interpretation (typically all runs of a program) and so this evaluation affects I, the interpreted system.
Kai gave an example of a paradoxical knowledge-based program derivation. Pretend that assignments were expensive and that we wanted to make sure that we actually had to assign before we did it. He showed how a paradoxical program had no implementation in the knowledge-based system.
To solve non-implementability, we generalise the program to address the difficulty of finding implementations and the complexity of implementations.
To solve the lack of abstract actions and proof theory we aim for a refinement calculus supporting reasoning on knowledge.
To solve counter-intuitive assertions you do something that I missed because my fingers couldn't write fast enough.
We swap our knowledge operators for existential quantifiers which makes the revised program implementable. To abstract these actions we introduce an architecture-independent action "Notify{i,j}(O)" and knowledge transitions. These are generalised by specification statements [KiO; Ki <> KjO]. This is read "i does something so that, later, j knows O".
Kai gave the example of Little Nell being tied to the railway track. [T, <> O] == "go from any state to O" (where O == "Nell is safe"). Dudley Doright comes along to save her, as specified. But the existing model allows Dudley to do nothing, and Nell gets squashed! [Cue graphic animation]
Introduce constraint tags to save Nell. These force the conclusion that some action is required. Kai described the assertion language L and the grammar for programs with n agents. This language is called "Prg"; it has a synchronous semantics. Programs occur over sets of intervals and an implementation. He skipped over details of the refinement rules due to time.
To drop the synchronicity requirement:
Kai introduced the fork() operator (as per Unix) and gave example of a bit transmission using fork(); will be pushing the use of fork() in the future.
[Tables are a bugger to transcribe into ASCII, by the way.]
Tables are useful for verification and refinement. They provide a natural way to decompose manipulation of propositions and their rules are easier to memorise. Example:
p | q | r -----+-----+----- s | t | u
equivalent to (p and s) or (q and t) or (r and u)
The general 1-d table has the form:
pv -- qv
where pv, qv are vectors; this is equivalent to forall i: (pv{i} and qv{i})
The general 2-d table has the form:
| qv
----+----
pv | rm
where rm is a matrix; this is equivalent to forall i,j: (pv{i} and qv{j} and rm{i,j})
Emil gave examples of basic operations such as splitting and joining:
| qv | rv | qv | rv
----+-----+----- == ----+---- v ----+----
pv | qm | rm pv | qm pv | rm
extending / contracting:
| qv | rv ( | qv | rv ) | qv
----+----+---- == ( ----+---- == ----+---- ) => ----+----
pv | qm | rm ( pv | qm pv | rm ) pv | qm
and lifting 1-d to 2-d:
pv | pv ---- == ------+---- qv true | qv
The equivalent text expressions are large and complex.
Emil described the formalised notions of disjointedness and coverage:
pv is disjoint if !(pv{i} and pv{k}) forall i != k
pv covers condition c if forall i: pv{i} == c
He gave examples of making a table header disjoint and complete, and gave simple rules of table transformation such as negation. He then moved on to illustrating tabular relations:
| QV
----+---- = union{i,j} PV{i} n QV{j} n RM{i,j}
PV | RM
Relations from X to Y are functions of type X -> Y -> Bool. A tabular relation is standard if all headers are conditions and inverted if the body and all but one header are conditions. Emil gave an example tabular relation for an elevator.
NB: while consistency and completeness of a specification depends on a problem domain, disjointedness and coverage properties help in formulating these.
Emil defined operations on tabular relations e.g. composition operator '.' and the domain operator '/\' (Delta).
How do you verify? Interpret the relations as nondeterministic programs and find the weakest precondition of program P to establish C:
<P>C = !(P . !C)
| CV / | CV \
----+------ = < ----+---- > C
BV | <PM>C \ BV | PM /
where (<PM>C){i,j} = <PM{i,j}>C and BV, CV are complete and jointly disjoint conditions.
He gave a reduced result for non-complete, non-disjoint conditions and gave an example of NR ("No Requests") predicates in elevator program, checking if NR is preserved if the button is pressed.
He also illustrated vector (predicate) tables; these have a 2-d structure but defined in terms of a 1-d table, like a conditional assignment. You can give a simplified rule to calculate the weakest precondition.
Emil illustrated how data refinement works, using an encoding operator (Q
down R):
P (= (Q down R) => (R.P) (= (Q.R) if R is injective.
If the refinement relation is given by an inverted vector table then the header defines the concrete invariant and the body defines the abstract function. He gave an example of refining an abstract queue to a concrete queue.
Conclusions:
Operation of extracting a specification set from the maximal sets was described; it allows us to reuse the text of a specification set and construct new specs by instantiating them.
[It was about now that my set algebra started to prove inadequate]
Conclusions:
Jim carried on Kai's railroad analogy; UML is tied to a railroad track and only formal methods can save her! He noted that there were about 60 partial semantics for UML, but nothing proper. It's not that hard to give a semantics to the interesting parts of UML, once you get past the documentation.
He described UML as a framework in which to place piece of specification. He noted the problems with using Z and CSP in industry -- where to apply them? How do you relate what has been done to the rest of the system? Some people try to formalise everything, which he views as a Big Mistake.
In Jim's view, UML is not perfect but is an OK framework and is well supported. It has a formal syntax but no formal semantics. The rationalisation for this is that the designers don't want a specification because "state of practice in formal specification doesn't address the language issues of UML", according to the UML committee. Yeeeeesss... "Every model can be expressed at different levels of fidelity."
But at times you actually care about the model so we can find a formal semantics useful for consistency and properties checks. We could generate a test suite based on the state machine semantics of the model (the AGEDIS project is taking this approach.) We can define a behavioural semantics by mapping models to processes in a machine-readable version of CSP.
Almost every UML model Jim has constructed has been wrong! It's very difficult to get a model's behaviour just by looking at a diagram. Tools will be vital for any significant system.
Jim broke down the four kinds of diagram:
So how do you use refinement based on this?
We could use refinement relations to compare two models of the same component (where a model is a collection of diagrams probably associated with a description of some component).
If models M1, M2 have different class diagrams then it is hard to achieve a failures refinement since the concurrent invocation of operators screws the shared state. There are 2 concurrencies in UML:
Jim noted that state diagram notation was inherently single-threaded. Relax this and BANG! you're shafted. You can't reason about it any more, it's too complex. So you can't have concurrent invocation of operations. He showed how in the example a normal approach failed.
But if you put the protocol and transceiver modes in a single-threaded context then you are OK.
This talk looks at end-based choice. The motivation comes from hierarchical system development, and from "speculative" concurrency to reduce unpredictable latencies e.g. in the WWW.
Action refinement is an important model for system development. Harald's model is "extended bundle event structures" ("ebes") which allowed interruptions. He sketched out a diagram showing events associated with actions and an action labelling function. I didn't really understand where he was going with this.
He contrasted start- vs. end-based refinement and illustrated with a simple graph example that composed to different event structures. Equivalences identify event structures with the same behaviour, but in both start- and end-based systems most equivalences are not preserved. So which ones are?
He looked at trace equivalence, which needs the relation of initial events after every execution to get congruences and keep the relation during execution. Two ebes are defined as initial corresponding trace (ICT) if every initial event trace has an isomorphic trace in the other ebe. He showed graphic examples of this and asserted that ICT-equivalence implied trace equivalence, and is a congruence for the end-based refinement operator (and other standard operators).
Harald aims to extend ICT-equivalence to get a congruence relation on bisimulation, and gave a fairly complex definition of the requirements for this. He showed examples of UI-equivalent and non UI-equivalent ebes, noting that UI equivalence is a congruence for the end-based refinement operator. Finite UI-Bisimilarity was described similarly. He showed the hierarchy of equivalences from the most discriminating to the least.
He noted that action refinement was well established in untimed event structures, and now he's looking at timed systems:
How can actions be defined in timed truly concurrent systems? Use the aforementioned timed (bundled) event structures ("tes"). He showed an example of a tes graph.
[About now I started to suffer from algebra poisoning and most of the rest of the talk drifted by in a haze]
For configuration refinement we replace each event of the observable configuration by an observable configuration of the refinement, where the time has to be adjusted. Harald gave an example of process refinement but the motivation was still unclear.
Conclusion: the same framework for action refinement also works for stochastic and probabilistic processes.
John Derrick closed the workshop with some concluding remarks; he'd found it a very interesting workshop, and commented that it was nice to be part of FME and FLoC. The aim of the workshop was to revitalise refinement, which seemed to have worked, and he intends to set up another one in the future.
I caught the bus back to Norreport Station and the train to Kopenhaven Station -- the wonders of cross-ticketing, Railtrack please note -- and left my case in the luggage lockers to free me up to explore the city. Heading on up Stroget the sun was bright and the sky blue, though clouds threatened. Last time I was here I hadn't really looked around the Kastellet and was determined to address the oversight.
On the way up I routed through the palace and noticed that the guards actually were allowed to talk to tourists, though apparently not to deviate from their patrol. The Buckingham Palace guards could teach them a thing or two...
The Little Mermaid was ringed by tourists this time, and getting photos was trickier. I managed what might have been a couple of decent shots eventually, and walked up to the northern end of the Kastellet. I took the west side walkway along the ramparts and admired the moat and surrounding greenery in the bright July sun. Some goats were grazing happily down at the water's edge; presumably these were highly trained Danish Army attack goats.
At the south entrance was a very small museum dedicated to the Livjaeger volunteers. Chatting to the curator I discovered that the regiment used to be a joint command with the Finns (Sweden's army was conscript) until WW2 when armistice terms made Finland discontinue the regiment. The curator also gave me a potted Danish military history. I hadn't realised that Britain had invaded Denmark so often, nor that we'd invented city bombardment in 1807 while raiding Copenhagen. He didn't seem to hold it against us, which was nice of him.
Heading back along Stroget hunger started to bite so I ducked into an eaterie near the Radhusplads for hakkeboef and egg -- basic but tasty -- and then over to Baresso for coffee and a muffin. <rant>Why does everyone have to show off their English? If I ask for something in Danish, and you understand what I say, what the heck is the harm in replying in Danish? Huh? How the hell are people going to learn Danish if you insist on speaking English to them all the time?</rant> [Sorry, it just gets on my mammary glands.]
The 250S took me back to the airport. Another point for Copenhagen's transport system -- the buses to important places run every 10 minutes even on Sundays. The calling for the Go flight back to Stanstead was delayed so I got a couple of magazines out of the newsagent's (not high literature or anything -- "The Economist" and "Maxim") and chilled.
We boarded half an hour or so late, but the crew was efficient in getting us onto the runway and the flight made up time. I was swilling coffee to keep awake and alert, mindful of the drive ahead. Luckily the baggage handling was quick, and I was in my car before 11pm.
The M11 away from Stanstead was quiet, as was the M25 and M4. I stopped just south of Reading for a sugar and coffee break, then pressed on towards Chippenham. Eventually I pulled up in Bradford-on-Avon coming up for 01:30, tired but pleased to be intact.
I checked my email before retiring for what remained of the night. Another paper of mine had been accepted for the RHAS workshop at RE'02 in September. So I've got to do all this again...