This was transcribed from illegible notes made by hand as I tried to follow what the speakers were saying. So there is <UNDERSTATEMENT LEVEL=GROSS>the possibility of some inaccuracy</UNDERSTATEMENT>.
Usual disclaimers apply: the opinions or research of anyone mentioned here may quite possibly bear no reality to my understanding of them. If you're using this as a reliable data source, you are quite mad. But it hopefully gives a useful flavour of the conference, which I found enjoyable and interesting.
The option of spending two hours behind the wheel of a car on the M4, followed by trying to find a space in the Heathrow short-term parking lot, hadn't appealed. I took the early morning train out of Bath to Reading, packing a laptop and my well-worn flight bag. At Reading I switched to the Railair coach for a cruise over to Heathrow T1. All in all it was impressively hassle-free. No delays to speak of, and a relatively comfortable journey. Definitely an option to consider for future excursions.
Heathrow T1's departure lounge hadn't got much more character since last time I'd been in it, but at least there was plenty to look around. I ended up with a sushi tray from Pret-A-Manger and Tom Clancy's latest book (Red Rabbit) -- not great literature, but then for travelling I find I just can't bring myself to read anything cerebral. As brain candy, it was just the ticket, and there was plenty of unintended amusement as I read Tom's latest attempts at British dialogue. After a year in New Jersey, I could speak just enough dialect to know better than to try writing it. Maybe Tom needs a similar excursion to England.
The flight to Düsseldorf was about an hour and a half. Compared to the Denmark trip the other month, the food wasn't as good (a sandwich plastered with everything I didn't like) but at least I could understand both versions of the cabin announcements; my German hadn't rusted as much as I feared.
Düsseldorf airport itself was almost painfully modern. Picking up baggage from the carousel was straightforward; it was noticeable that all the men had noticed the direction of the conveyor belt lapping and moved to the wall hole where the luggage would emerge, whereas the women were scattered all over. Transport to the main airport railway station was via the new Sky Train suspended monorail, which was a very hi-tech way of getting around.
I'd forgotten what German train timetables looked like, and it took a few minutes of figuring to work out what line I was looking for, but I finally located the platform for Essen and bought a 1-way ticket. It insisted that it wasn't valid unless stamped, but I couldn't spot a stamping machine for the life of me. Oh, well. The train itself was on time to the second, uncrowded and comfortable. I relaxed and watched the countryside go by.
Essen Hauptbahnhof was quite busy even on a Sunday, and it took more figuring to understand how its U-Bahn tracks worked, but for 1 Euro I could travel up two stops and walk a leafy, sunlit path on quiet town roads to the Hotel Europa. At first sight this hotel seemed horrific -- its main entrance was at the side of a multi-storey car park -- but in fact, once you'd taken the lift up to its lobby above the car park it was quite pleasant and comfortable. The staff were friendly and -- praise the Lord -- replied in German when I spoke to them in German. My room was small but cosy. I plugged in the laptop, ran through my presentations for the next day, and washed off the grime of travel.
With the evening falling I wandered into town in search of food. The hotel turned out to be ideally placed, within comfortable walking distance of the main shopping street.
I eventually settled on an outside table at a relatively non-descript eaterie and went for beer and a cheese-covered steak. The sky darkened, but it stayed relatively warm while I ate, watched the passers-by and listened to the banter from nearby tables. Several gents at the table next to me were having an energetic discussion about economics and politics -- the words were familiar from A-level German, though the details of the conversation went straight over my head.
On the way back, irony of ironies, I was stopped by
a middle-aged German gent wanting to know where the station
was. How long had it been since Mrs. Glendinning had taught
our class "Wie komme ich am besten zum Bahnhof, bitte?"
Now
the first time I had needed to employ it, I was answering
the question instead of asking it. "Gehen Sie geraderaus
ungefähr hundert Meter zur Hauptstrasse, drehen Sie
rechts um und danach zwo hundert Meter zum Bahnhof..."
At the hotel again I flicked through the available TV
and found a Leslie Nielsen ("Dick Steel") dubbed spy spoof.
Was die Hölle, I had nothing else to do and the rest
of the programming was tediously election-oriented so I
watched the film. Not too bad -- again, total brain candy.
My brain needed a rest before tomorrow.
Monday 9th September
There's something brutal about getting up before 8am in a foreign city. Today was no exception. Slight carelessness in turning on the shower (just how many different ways are there of designing heat/volume controls for water flow?) resulted in a gush of freezing wakedness before I could shut it off, gasping in shock.
Breakfast itself, in a sunlit room overlooking north Essen, was a pleasant affair. The coffee was OK, and the buffet was comprehensive. I always eat more at European breakfasts than at home in Britain, I don't know why. Today, my excuse was that I needed the energy.
I took the U-Bahn one hop north, then oriented myself and walked up the western edge of Essen University. The RE conference registration itself was at the northwest corner and it was a brisk stroll before I got to it. I arrived to find the registration desk crammed with patiently queueing delegates. They'd split registration by surname letter (A-K and L-M); strangely, there were many more in the A-K line than the other. Go figure.
Jon, my supervisor, appeared as I was nearing the desk. He was clearly an earlier riser than me. He was looking around for the RHAS workshop, but the directions weren't exactly clear. Once I'd got my registration pack (including a rather nice RE'02 mug) we consulted the maps and headed out in search of the room. It took a good ten minutes of footling around before we could make sense of the maps and find our way into the remote part of the campus to which the workshops had been consigned.
Our timing was, unlike our navigation, impeccable. We arrived
just in time to set up laptops before Connie Heitmeyer from
NRL opened the workshop.
Introduction
Connie outlined the RHAS topics:
She defined a High-Assurance System (HAS) as one in which
"compelling evidence is required that the system delivers
services in a manner that satisfies certain critical properties."
With reference the Heitmeyer-Rushby paper of 1991 she listed the
main classes of HAS:
Why choose "high assurance" as the workshop title? Because HASs are quite specific; we can distinguish them from other systems. Failure costs are high: death or injury, damage to physical system, does not deliver services (on time), compromises national security, economic loss.
It is never enough just to build e.g. a safe system; other properties are usually needed.
The goal of this workshop: discuss issues relevant to acquiring,
specifying and analysing high assurance system requirements,
not requirements in general.
What process to follow
Chair: Martin Feather, JPL.
"High Assurance Requires Goal Orientation"
KAOS theory from Axel van Lamsweerde and Emmanuel Letier (Uni Louvain, Belgium). (NB: this complements Connie's approach; it's not intended to oppose it.)
Why is requirements engineering hard? The problem comes in elaborating requirements:
So if you want to do RE, how do you do it?
An example is the London Ambulance Service requirement that 95% of calls receive a response within 14 minutes, 50% within 8 minutes. It's hard to reason about this kind of requirement.
Axel and Emmanuel are working on goal-oriented requirements engineering with KAOS.
Gave example of needing to shut down a reactor when coolant is lost:
[There was a lot of frothy discussion about what granularity of agents was appropriate -- Martin interceded to bump the talk back on track.]
MF noted that the RE focus is more about "how do we know unambiguously that loss of coolant has occurred?".
The purpose of the KAOS model is to start with something like this and carry it through to ensuring that things are done reliably. Connie asked for clarification on the relationship between KAOS and SCR in the RE timeline.
The example of the LAS assumed that the system would always know where each ambulance was. Wrong! They needed in-service protocol changes to overcome these faulty requirements.
Q: [Betty Chen] Are all goals safety goals, or can you have others
e.g. functional goals?
A: Yes! KAOS was used to model the California Bay Area Rapid
Transit (BART) system (and also for the UK NATS air traffic control
centre at Swanwick).
SCR
Connie Heitmeyer, Naval Research Labs.
SCR is an operational approach to RE as opposed to KAOS's goal oriented approach. So:
SCR is based on state machines and tabular functions. It looks like:
Define problem <--------- Design solution
(system goals) | ^
| ^ | |
| | | |
v | v |
Assumptions and --------> Specify solution
assertions <-------- (SRS)
Developers capture the solution precisely and umambiguously in a "build-to" solution. We differentiate between the model and the specification.
"A rational design process -- how to fake it."
Instead, throw away the system design. Why?
Experience of using SCR has included systems such as:
Q: [Jon Hall] Is the problem of scaling up a RE process really a question of the scalability of expertise in a system / process?
Q: [Martin F] Why are clients willing to buy in to KAOS/SCR? What
motivates them? What are they afraid of?
A: [Connie] Testing and a good SRS implies the ability to
autogenerate tests from a specification that satisfy some coverage
criteria. Lots of time and money is used by software testing.
[Although the Praxis perspective is somewhat different - Ed].
Connie observed that tables are quite open and readable for users. She noted that people tend to use SCR when they have a good idea of what the requirements actually are. She has found it very hard to find out what system assertions are from users e.g. safety properties.
Emmanuel noted an example of ambiguity in the area of train-automobile
collisions at track-road crossings, which would not be present in
Connie's model.
The role of formal methods and tools
Ramesh Bharadwaj from NRL chaired this session.
Formal Analysis of Domain Models
Ramesh presented this talk. He discussed a case study of using formal methods in a lightweight manner. [He used very small text on the slides which made taking notes quite hard.]
Specifying a system at the correct level of abstraction:
He's looking at "relaxing the domain to get a more feasible environment" [uh? - Ed].
Specification: distinguish "what" vs "how".
Case study of a flight management system speed mode indicator. Based on the paper by Leveson et al at ICSE'02; this case study rewrites the requirement specs in that paper.
We avoid overspecification and underspecification if an
implementation X is such that:
X satisfies customer <=> X satisfies specification
Other attributes of a good specification include:
Ramesh summarised the history of the SCR method and clarified its notation. Their are four constructs:
Axel and Ramesh agreed that state machine diagrams (especially UML) aren't generally clear on what's happening, especially with respect to monitored and controlled variables.
The domain model is a partial description of the required behaviour of the system, built specifically to find answers to certain questions - the "what if" rather than the "when" or "how".
SCR toolsets can check syntax, type errors, specification consistency, and find answers to specific questions. Ramesh applied this to the speed mode indicator example. Noted that you have to write "type dictionary" (i.e. variable type ranges) rather than "variable directionary" (which maps variables to type).
Martin F defended the original (Leveson) SMI example; four specs in a 10-page paper so it's hard to make them clear to everyone! Ramesh went off in a mild tirade against paper authors not putting full specs etc. up on the web for public checking.
Ramesh showed the mode transition table for the SMI example to show how much clearer it was. There was a comment from the audience that the generational change in programming languages (asm to C to Java) means that many developers are now no longer able to understand certain forms of specification, which was a fair point. Axel observed that you don't have any structure in these specifications, which is what makes them hard to read; also a fair point.
Nancy Mead asked whether anyone had actually checked which forms were easiest for users to read? Connie said that some work has been done with other specification forms with grad and undergrad students; graduates can generally understand specs, but undergrads can't. Christophe noted the need to know the technical background of the group; Ramesh said that half of them were domain experts (comp sci students).
Ramesh pointed us at Q.2 in the paper in the proceedings; can we the audience answer it? Not obviously; it's a hidden transition. The tool tells you that it's OK, so inspections by themselves are clearly inadequate.
Q: [Betty Cheng] how does one distinguish properties of the spec from actual goals?
Q: [Christophe] how does the ordering of question terms work?
Conclusions:
Q: [Jon Hall] How would you go about proving freedom from e.g. race
conditions?
A: You can check for no ambiguous transitions.
Followup comment: note that we only consider validating
consistency of the model, not the system.
What About Industrial Control Software and IEC 61131-3?
Bernd Krämer, Fernuniversität Hagen
IEC 61131-3 refers to programmable logic controllers (PLCs). Bernd is addressing RE within these devices. He said that he didn't want to respond to the beauty contest earlier [thank goodness - Ed]. The key points he extracted from Ramesh and Nancy's papers:
He noted that:
He gave a run-down on the background of industrial control programming. Certification by public authorities is required; currently the authorities want exhaustive testing but of course this is inadequate in most cases! (Connie noted that common criteria also exist).
He gave an example of an actual system and the notations used to describe it. Functional Block Diagrams were coupled with Sequential Function Charts. He noted that there were lots of standardised function blocks in the standard library.
So there is a need formal methods in the area, but still a big gap in terms of practicality between RE, the engineers and the certification authorities.
Open PLC site: www.plcopen.org. Noted that Dave Messerschmidt from UCB has also presented on this topic.
Jon Hall commented that the Hilton and Hall paper (120Kb PDF) in the proceedings specifically addresses a number of these issues.
Betty commented that her undergrads have problems due to UML not
having processes or anything associated with it; you need a process
for each separate industrial domain.
RE: Are Formal Methods Ready for Industry?
Michel Lemoine, ONERA. (ONERA is a laboratory looking at the aviation and space industry; Airbus is one of its customers.)
Note:
Current problems are:
Q: why can't they?
A: a question of organisation.
Current practice:
Can we customise formal notations for industry?
UML is a partial answer; Michel isn't totally in favour of
it, but it's a start from the point of view of understandability. We
can identify problems with it, but not correctness.
Michel suggests complementing UML by formal notations.
The role of UML
Betty Cheng from Michigan State Uni chaired this session. There were no paper presentations; instead, she proposed three questions:
She had asked three people to respond to this, and had added Michel
Lemoine to the list after his earlier
presentation.
Sascha Konrad (Michigan State)
He was looking at "Requirements Patterns" (similar in concept to the in-vogue Design Patterns). He extended the requirements patterns template with use cases, constraints, behaviour, design patterns. The domain is embedded High-Assurance Systems.
Challenges:
RP is aimed at the industrial use of OO and UML for requirements capture and validation.
Q: [Connie] Why the use of OO (a data-focused approach) when HAS
designs tend to be heavily control-oriented?
A: [Christophe] OO has a range of components and developers can
use some of them without using others. [At this point Axel and Ramesh
went off on the old KAOS-SCR dispute].
Q: [Connie, rhetorical] How long-lasting will the use of OO and UML be?
BMW and Gephard have structured their RE activity as follows:
So workshop Q1: use use case diagrams for elicitation.
At this point Michel and Axel went at each other about the semantics of UML, which eventually became an excellent example of a fundamental problem with UML in HAS; lots of fundamental ambiguity in its diagrams. Martin F did an excellent reductio ad absurdum on the issues under argument.
Looking at Q2, what arguments against UML are there? The main one is a lack of formal semantics, so address this by:
Q: Do you define semantics for UML:
A: Yes.
Q: But everyone does their own map and so defines their own
semantics...
A: Yes -- the UML committee says that this is OK. So every
domain has its own mapping, and maybe even every company!
Ramesh commented that at least C has a well defined semantics. "Oh no, it doesn't!" I replied. Syntax, maybe, but definitely not a well-defined semantics -- even Ada doesn't have this.
Non-functional requirements can't be captured easily in UML. Address this by using our mapping to check for some non-functional requirements e.g. safety, omission of deadlock. Timing constraints are also hard to express in UML. Current work on this involves trying to extend the formalising approach to timing parameters in UML and modelling Quality-of-Service properties e.g. maximum response time.
Addressing Q3, the arguments in favour of UML:
So:
He gave a case study on a fault protection engine for a spacecraft. Inputs are "symptoms", executes "responses". It's a generic model for all spacecraft.
The responses are defined by little statechart diagrams which control items on the spacecraft; it uses autogenerated C/C++ code but the engine is much more complex so autogenerating this won't work.
They don't use statecharts as code generation tools are inadequate; the robustness of the tool is as important as the language choice.
UML helps to get people up to speed but doesn't replace access to the designer. But if you restrict yourself to a small subset of UML then it's easier.
Q: what sort of simplification of UML do you do?
A: Allow nested states, but not concurrent states.
Jon Hall (Open Uni)
Jon turned the questions on their head by taking a view of a HAS and trying to work out what UML should be / have in order to support it.
Does it:
Will it be mandated? It faces stiff competition from e.g. Z.
Comment: [Connie] Should we start by assuming UML is a de facto standard, or start with a problem and then select appropriate tools? Apparently, UML is in the critical systems interest group! Connie has had a hard time finding out from papers what the system was supposed to do.
Betty asked what industry people think of UML? Can we use it, or are we looking at alternatives? Answers from the industry people in the workshop included:
Nancy Mead from SEI chaired this session.
Nancy defined the relevant terms. The focus of survivability is on the system's mission:
Survivability is defined as "the ability to fulfill the mission in a timely manner in the presence of attacks, failures or accidents." There are three R's of survivability:
Intruders are viewed as users.
The technical issues of survivability include:
Practical issues include:
I presented the safety-critical systems approach to survivability. Key issues about survivability in real-time safety-critical systems that I identified included:
There was general interest in the concept of safety integrity
levels (SILs) and how we could reason about probabilites of failure.
Emmanuel Letier
Emmanuale took a goal-oriented perspective on survivability, identifying obstacles to goals and how to avoid them:
He gave example of a credit card transaction authorisation, which looked to me like a reverse hazard analysis in essence. He noted that knowing when to stop in this sort of analysis is a real trick. The overall plan is:
We try to build a catalogue of obstacle resolution tactics to eliminate, reduce or tolerate obstacles, and monitor our goals at run-time.
Connie commented that we need to identify the failures to design for, the way that Praxis do. She also noted that network management clients haven't devoted much though to attack, but lots to failure.
Christophe commented that he'd looked at the Überlingen
aircraft collision of July 2002, using KAOS to analyse the accident to
see if it was a TCAS or ATC problem. This showed how many failures
were needed to cause the crash [which seems to confirm Leveson's event
chain analysis approach - Ed]. There was a bit of confusion from the
audience about the probability theory aspect of this, confirming once
more that it's not the easiest of areas to understand.
Wrap-Up
Connie gave the wrap-up and thanks. She proposed that the chair of each session do a 1-page description and send them to Nancy by October 1st, and each presented to send copies of their viewgraphs to Nancy. Paper references should be included in the annotated slides.
A potential RHAS'03 workshop was discussed; the floor is open for themes to be discussed, such as focussing on particular classes of high-assurance systems.
After the day's session I walked back to dump all my notes and books at the hotel before meeting up for a bite to eat and a beer with my supervisor. The workshop went pretty well, overall. It was surprising to find out just how directly applicable high-integrity system safety techniques were to the problems being discussed. In particular, the issues introduced by survivability in high-assurance systems seem worth a good hard look. Something to bring to RHAS 2003, perhaps?
Adrian Hilton, October 2002