by Michael Blume
| University of Bielefeld - Faculty of technology | |
|---|---|
|
Networks and distributed Systems
Research group of Prof. Peter B. Ladkin, Ph.D. |
|
| Back to Abstracts of References and Incidents | Back to Root |
|
Harold Thimbleby
Computing Science Middlesex University GB-London, N11 2NQ | & |
Peter Ladkin
Technische Fakultät Universität Bielefeld D-33501 Bielefeld |
We demonstrate a simple language that combines specifications and manuals. This shows: first, that a user manual can be automatically reconstructed from a logic specification that is effectively identical to the original logic (up to ambiguities in natural language); second, that such an automated process can help detect errors. The process is fast, and suitable for use in participatory design.
29 February 1996; revised 5 September 1996
It is widely recognised that requirements change and systems evolve, amongst other reasons because of design needs, and in response to user feedback [SwaBal82] [Boe86]. In systems where users form an essential part, it is common practice to involve the users in the design process. As users increasingly understand a system, they may help change its design for the better. Logically accurate user documentation is desirable in itself, and a reliable, fast method for generating it could improve the design-trial-redesign loop. We describe a simple prototype tool, implemented by the first author, that accomplishes this.
Aircraft control and flight management is a human-in-the-loop system. We use it as an example in this paper, partly because some actual user manual pages have been reverse-engineered by the second author [Lad95] and now exist in a form on which we can demonstrate the forward-generation of new manual pages; and partly because it is pilot folklore that Flight Crew Operating Manuals (FCOMs) are in constant need of improvement [Buc94]. However, the technique we illustrate is applicable to derivation of accurate documentation in general, and the tool we describe is not limited to particular types of systems.
Deriving documentation from specifications is not new. [LevHeiHil94] and [HeiLev96] describe the provision of full formal requirements specifications for TCAS II avionics systems. [ParMadIgl94] and [ParMad95] describe the documentation of the software design process: "The validation of design documents [...] is a major part of engineering. [...] Documentation can be used both as a design medium and as the input to subsequent analysis and testing activities." The IDAS project [ReiMelLev95] aimed to derive technical documentation in readable natural language, aimed at "technicians and other experts [rather than] 'the man in the street' (e.g., aircraft maintenance manuals, not VCR operations manuals)". In contrast with Leveson et al., we do not aim to document requirements. In contrast with Parnas et al., we do not aim to document a development process for engineering purposes. We do aim to support the provision of a complete, consistent, usable end-user manual for a process-control system. We assume the system requirements and development as given. In contrast to the IDAS work, we do not aim to automate the production of natural language instructions, and we are more concerned with documenting real-time systems to enable timely user response in changing situations, such as needed in FCOMs. This does not preclude eventual synthesis between the approaches.
With the introduction of so-called fly-by-wire airplanes in commercial transport, avionics now encompasses all aspects of piloting. A pilot of such an airplane is interested in what the specification says about only the state variables that are immediately 'to hand' - say, position of thrust levers and its relation to measured engine power - and their changes. Other variables such as those describing, say, engine fuel-flow controller state are more important for design and maintenance engineers than for flying the aircraft. So the pilot's view can be regarded as an abstraction of the design specification of the whole aircraft, namely a predicate in a restricted vocabulary of state variables that is logically implied by the design specification.
It is important to distinguish the particular needs of an operator from the general need to document the development and design of a system. An operator will in general not care how, or using what process, the system was developed. A pilot only cares how the airplane functions right now and how to control it. A pilot flying a landing go-around will use features of the design (position of the controls, for example) in order to command the aircraft to fulfil certain requirements (in this case, performance requirements). One can expect an operations manual thus to contain information from both requirements and design.
We are interested in deriving end-user manuals from requirements or design specifications. The meaning we give to the word 'specification' allows a precise, correct statement of what the operator 'sees' also to be described as a specification. A system may thus have many specifications of this type. (We take it as one of the advantages of the logical approach to specification that it handles this form of abstraction so trivially.) The FCOM is an important end-user document recalling essential information for the pilots, and is legally required to be on board an aircraft in flight. It omits information maybe necessary for engineering but of little help in the cockpit, as well as much information on the system design pilots would have learnt in a training course. A crucial feature of the FCOM is that the airplane (and the pilots!) should behave exactly in the way detailed in the FCOM. The FCOM thus should be a specification in our sense, for some part of the total behavior of the aircraft.
The second author [Lad95] analysed part of the FCOM for the Airbus A320 airplane from this point of view as a logical document. He showed that the FCOM for a particular A320 (the one reported in [MCAAI94]) has shortcomings if treated as a rigorous definition; namely, ambiguities and omissions. He rewrote the FCOM pages concerned as Predicate-Action Diagrams [Lam94a], a way of describing finite state machines in which states and transitions between them are labelled with predicates with precise semantics in the Temporal Logic of Actions (TLA). TLA is a temporal logic designed for system specification and verification [Lam94b].
What we regard as logical shortcomings in an FCOM may have origins in the conflicting needs of pertinence, coverage and brevity, as well as in simple error. Some shortcomings may arise from a psychological judgement of how best to promote recall of systems and emergency procedures that pilots have learnt in training but are seldom required. Desiderata for operating manuals may thus conflict. However, we suggest that consistency with specifications is not in conflict with any other desideratum. We call such a manual accurate. (It follows that accurate manuals must be specifications in our sense.) To fulfil other desiderata, a method generating accurate manuals should allow optimisation possibilities according to different criteria. Our method does this, starting from specifications whose accuracy we assume is given.
There is a legal requirement in aviation for accurate flight crew operating manuals. Buck [Buc94] strongly makes the point that manuals frequently fall short of what pilots need in a difficult situation, that pilots in such situations often must improvise, and that this is becoming particularly difficult with the introduction of complex avionics. Avionics systems can be considered interactively complex and tightly-coupled [Per84]. A suitable illustration may be derived from a recent accident to a Birgen Air Boeing B757 aircraft in February 1996 [Lad9x]. There are two relevant features of this accident, which illustrate the difficulties of writing quickly-usable manuals when the system is interactively complex.
We demonstrate the tool by taking the re-engineered logic specification of the A320 braking subsystem from [Lad95] and construct precise FCOM pages from it, below. Apart from their precision, these pages are comparable in content and structure to the original. Their layout is also comparable, though we chose to use tables rather than bullet lists (as are used in the FCOM). When our automatic construction techniques are applied to appropriate specifications, the result is also a specification, presented in a more human-oriented way.
This entire paper (rather, its electronic version as submitted to this Journal) is itself the result of a single actual run of the tool. The example input is included as source, along with the text body of the paper as meta-comment (see below). The output of running the tool on the source of the paper then yields the text, the example input, plus the output to the examples, formatted as you read below. We did no cut-and-paste on the examples, nor any other post-editing of the paper.
The system is simple, and so are the examples. But that's partly our point. Specifications of user interfaces of critical systems are designed to be simple. We are describing a preliminary tool that handles examples of the appropriate order of complexity. However, in the average FCOM, there will be many such examples. Keeping track of the interconnections can be complex without automated help. This is partly why the traditional 'by hand' approach to manual writing is prone to lose rigor.
The usual benefits of automatic generation include the ability to maintain a correct manual under changes of the specification. This aids in collaborative design [Thi96], in which users are involved in assessing designs and hence improving their effectiveness or safety, as practiced with human-in-the-loop systems. We have mentioned that our approach facilitates the design-trial-redesign loop. In principle, this could be extended to concurrent engineering, in which technical authors would maintain documentation and evaluate it with operators at the same time as engineers maintain a complete system specification. We have discussed elsewhere techniques to allow technical authors to improve the quality of language used in manuals without compromising the guarantees of automatic generation [ThiLad95].
Our language has Boolean expressions, using !,
& (or dot), +, => and
<=> as the
Boolean operators not, and, or, implies, equivalent; others are easy to add.
Operator precedence is standard; association is to the left. Two print operators evaluate
and print minimised expressions: >e prints a minimised equivalent to
e; and ?e prints a minimised
and factored table in HTML (the hypertext markup language used on the
World Wide Web [NCSA96]).
In addition, rewrite rules can be used to simplify expressions. A rule
of the form r := e allows that the
expression e is rewritten by
r. Since rewrite rules may overlap (as in
r:=a&b; q:=b&c; ?a&b&c;), their
application requires minimisation. Use of rewrite rules
is illustrated in the examples below.
Since one may not wish to print an explanation of something that is
trivial, there are two more more operators. The slash makes printing
using either > or ? conditional; thus
>e/p prints a minimised equivalent of
e if p is true. Secondly, the
expression [e] reduces to true iff
e is a contingency (that is, iff
e is neither strictly true nor false).
The language also provides for name bindings, including functions. To
follow the examples below, we mention the following details: comments
are taken from % to the end of the line; variable names
are either strictly alphabetic strings, or anything between quote
symbols (including \" or \\ which represent
" and \ in the conventional way).
Our language may not be formally the most elegant or complete. It was implemented to prove a concept, and it works. We do not provide a formal definition in this paper for several reasons: the program is available from the authors, we would rather encourage others to develop our work rather than take it as definitive, and anyway - a point already emphasised - it is a simple system that takes only a week or two to implement. We would like to encourage other workers - particularly in industry - to adopt the concepts, not the specific prototype. The next sections give some examples of real runs with it.
input and output in
our examples:
}
% Use a long variable name...
>"This is a simple example using a function we define"
% Define a function equals (one of many ways to do it)
equals(a, b) = a + b => a & b
>equals(a, a)
>equals(a, true)
>equals( equals(a, b), equals(b, a) )
>"Equals commutes" / equals(a, b) <=> equals(b, a)
{Minimisation becomes more interesting when it is given problems that do
not reduce so simply, such as Exercise 1.16.A.3 from Zissos's textbook
[Zis72]
on digital circuit design:}
zissos = !a.d+!b.c.d+a.!b.(c+d)+!b.!c.!d
>zissos
{This result is different from the model answer, as the term
!c&!b is not given: there is a mistake in the Zissos textbook.
Further, with the automatically generated tabular form, we see that !b
can be factored out from two terms:}
?zissos <- "Zissos example"
{Note how the <- operator specifies a label for the table. The
same label is used in the glossary that is
automatically generated at the end of this paper.
Extract from original FCOM:There is additional prose in the FCOM that is descriptive rather than logical. It can be directly copied to the manual generator's output using 'long' variable names, as shown in the examples above, or by using meta-comment.
NORMAL BRAKING
Braking is normal when:Anti-skid is operative and autobrake is available.
- green hydraulic pressure is available
- A/SKID and N/W STRG switch is ON
- PARKING BRAKE is not ON.
Ladkin defined appropriate logical variables and determined the normal braking condition to be normal = green hydraulic and a/s and n/w strg and not park brake and antiskid and autobrake.
Writing Ladkin's formulas together with some explanatory rewrite rules gives the following manual specification:} "both power supply and BSCU operational" := !("BSCU failure" + "power supply failure") -> "Power normal." "both green and yellow hydraulic pressure insufficient" := !("yellow hydraulic" + "green hydraulic") -> "Hydraulics failure." "nosewheel steering switch is ON" := "n/w strg" "nosewheel steering switch is OFF" := !"n/w strg" % (some specification details omitted for brevity) {} normal = "green hydraulic" & "a/s" & "n/w strg" & ! "park brake" & "antiskid" & "autobrake" ; % Group lines of input together to get clearer output... ( > "
The tabular representation we chose is a minimal disjunctive normal form (DNF) equivalent to the original formula, with each line in the table being one term from the normal form. This representation closely matches the original form of the FCOM. The DNF lends itself to expressing precisely what the original FCOM chose to represent as bullet lists (one difference remarked by Ladkin [op. cit.] is that some of the bullet lists in the FCOM had obscure semantics).
We implemented the language with a minimisation algorithm that outputs minimised DNF, because it was useful for us. It is also a criterion that can be implemented precisely and optimally, and not confuse our claims with uncertainty over the exact nature of presentation heuristics. Minimal DNF helps, amongst other things, to check the logical meaning of desired manual entries, and that is what we wanted to try with the A320 manual pages. However, our approach is not beholden to minimal DNF. One can choose other features to minimise. One may prefer to output manual pages which satisfy other structural criteria (for cognitive reasons, say). We could also generate text that is not best presented as DNF. For example, many manuals contain conjunctions of implications, of the form:
((s11 and s12 ...) implies q1) and ((s21 or s22 ...) implies q2) and ...We do not know what users of manuals would like to minimise under what circumstances, though there is evidence (and supporting argument) that minimisation of some form is desirable [Car90]. For example, would users prefer to minimise the number of terms in a minimal expression, or the maximum number of factors in any term, or perhaps the greatest number of non-trivial common factors? There is scope for experiment, and we would guess that the results would depend on what users (in the current case, pilots) expect of the documentation. We do not wish to impose a particular answer. Indeed, one might provide a set of answers to accommodate various types of intended use.
In the following example, we first define a function possible(x) to be true if
x
is possible, that is, if x is true or is a contingency. Next,
if normal
mode without antiskid is possible, we output
the simple text "Alternate without antiskid and normal modes overlap when"
(i.e., treating it as a simple variable name). Finally, we output as a table the
conditions under which normal mode without antiskid is possible. We ran
this function as follows:}
possible(x) = x + [x]
normaltwout = altwout & normal;
(> "Alternate without antiskid and normal modes overlap when:"
? normaltwout ) / possible(normaltwout) <- "Overlap example"
{We discover that the FCOM description does not explicitly
account for power supply failure or BSCU failure modes. Thus
can the tool be used for completeness checking.
The current approach does not do this; it assumes the specification is 'flat.' However, extension would be easy, such as embedding it within an interactive hypertext system with some theorem proving capability. It would be important for any such extended tool to include various 'completeness' checkers. In particular, for a user to be able to request an abstract manual, the tool should be provided with a suitable summary of what information is not explicitly represented.
The glossary appears as follows. Any name, or head token of a rewrite rule, appearing in an explanation is linked to an entry created for it in the glossary. The glossary contains any descriptive text that has been associated with the name or rule, and also links back to the uses of the name. A user of a hypertext version of the manual can click on a phrase occurring in an explanation to obtain a full explanation of that phrase in the glossary, and similarly by clicking in the glossary move back to any use of the phrase in that or other explanations.
Beyond the clear advantages of a complete glossary, our approach closely associates glossary entries with the uses of the names (this is a 'standard' advantage of automatically constructed indexing). Thus it is easier to check the specification as it is being written, and built-in system checks ensure that all entries in the glossary are annotated.
The language provides three mechanisms to support the hypertext glossary.
Any name or rule followed by -> string has
string appended to its glossary entry. For example:}
"switch on" := sw -> "Mains switch."
"switch off" := !sw -> "Mains switch."
"Mains switch." -> "The switch is at the bottom of the red console,
pull it forwards to make it 'on.'";
{
Any expression followed by <- string is named
in the glossary (by the string) as the context of
use for all of the names in the explanation generated by the
expression. As mentioned above, the string also occurs in the explanations
generated, as a caption. The sense is that the right-pointing arrow puts text
further on in the document, into the glossary, and the left-pointing arrow
refers backwards from the glossary to the expression. In the HTML, of course, these
forward and backward references are hypertext links.
Finally, since manuals are often structured by sections, the same form without an expression defines a 'global context' for all following explanations - that is, as if they are in the context of a section with that label. The following example shows both forms in use:} <- "Mains switch example" > "
The glossary for all the examples is at the end of this paper.
The features of our language so far discussed allow a manual to be constructed from a specification, but do not allow the manual to 'talk about' the specification as an object in itself, which (for example) is what the text of this paper does, and what would be required in various specification documents as a system design is negotiated. Thus we built a 'meta-mode' for the language.
In normal-mode, the program processes all specifications precisely
as described in the examples. In meta-mode, however, it
processes specifications and additional text. The text is considered
as a 'meta'-comment. We have already mentioned the normal
'%' comment, and examples of its use appear in this paper
above. Meta-comment has no enforced typographical style, and the
comment markers (which are braces) are not represented in the
output.
This paper was created by meta-mode. The text of this paper, except the examples, was written as meta-comment. The text was input as 'source,' along with the input to all examples as described, but no output to any example. The output is the submitted version of the paper, which is identical up to typography to the version that the reader is currently reading, complete with output and glossary for all the examples. Evaluation in meta-mode enforces the font conventions for distinguishing input and output, to alleviate confusion. The actual source and output is available from both http://www.cs.mdx.ac.uk/harold/ and http://www.techfak.uni-bielefeld.de/~ladkin/.
Meta-mode is invoked automatically for any specification that uses meta-comments. If an author uses meta-comments in a source, to talk about the specification, the system generates a manual representing those comments, the specification, and the explanation. Meta-comments can also be commented out, and even those comments can be meta-commented, etc.
The manual specification language was first prototyped as an embedded language within Prolog. Not surprisingly, as minimisation, factorisation and rewriting are all NP-complete optimisation problems, the Prolog was too slow for practical use! The program was rewritten in C, and used the standard low-level programming trick of implementing DNF with up to 32 variables as a vector of 32-bit words, which gave it acceptable performance. Minimisation uses the Quine-McCluskey algorithm. There are many alternative algorithms that could also be used (including professional tools for optimising digital logic circuits).
The C program is limited in the complexity of queries it can handle (because the minterm algorithm can generate huge numbers of minterms). This has not been a practical limitation; one could argue that use of a specification that required more than 32Mb of RAM could involve such a degree of complexity that a mechanically generated manual would not help much!
We have done no research into the 'best' form of FCOM, one meeting all the desiderata in mutually optimal ways. Such questions would need to be addressed in any development of our work. We showed here that we could provide the FCOM material with logic and precision, by using an automatic tool. To do that we did not need to address the human factors questions. Our tool, particularly given its precise functionality, can be used in controlled experimentation.
[Bar96]: H. Barth, DiDoLog: Automatable Generation of Specifications and Formally Correct Manuals from Informal Sources, Diplom (Master's) Thesis, Technische Fakultät, Universität Bielefeld. Available through http://www.techfak.uni-bielefeld.de/~ladkin/. Back
[Boe86]: B. W. Boehm, A Spiral Model of Software Development and Enhancement, ACM SIGSOFT Software Engineering Notes, 11(4):14-24, August 1986. Back
[Bry88]: M. Bryan, SGML: An Author's Guide, Addison-Wesley, 1988. Back
[Buc94]: R. N. Buck, The Pilot's Burden: Flight Safety and the Roots of Pilot Error, Iowa State University Press, 1994. Back
[Car90]: J. M. Carroll, The Nurnberg Funnel: Designing Minimalist Instruction for Practical Computer Skill, MIT Press, 1990. Back
[HeiLev96]: M. P. E. Heimdahl & N. Leveson, Completeness and Consistency Analysis of State-Based Requirements, IEEE Transactions on Software Engineering, 22(6):363-377, 1996. Back
[Knu92]: D. E. Knuth, The TeXbook, Addison-Wesley, 1984, 1986, revised 1992. Back
[Lad95]: P. B. Ladkin,
Analysis of a Technical Description of the Airbus A320 Braking System,
High Integrity Systems, 1(4):331-349, 1995.
Also available from
http://www.techfak.uni-bielefeld.de/~ladkin/.
Back
[Lad9x]: P. B. Ladkin, ed.,
Computer-Related Incidents and Accidents with Commercial Airplanes,
Hypertext Compendium of sources and commentary.
Available from
http://www.techfak.uni-bielefeld.de/~ladkin/.
Back
[Lam94]: L. Lamport, LaTeX: A Document Preparation System, Addison-Wesley, 1994. Back
[Lam94a]: L. Lamport, TLA in Pictures, IEEE Transactions on Software Engineering, 21(9):768-775, 1995. Also available from http://www.research.digital.com/SRC/tla/. Back
[Lam94b]: L. Lamport, The Temporal Logic
of Actions,
ACM Transactions on Programming Languages and Systems, 16(3):872-923, 1994.
Also available from
http://www.research.digital.com/SRC/tla/.
Back
[LevHeiHil94]: N. Leveson, M. P. E. Heimdahl, H. Hildreth & J. D. Reese, Requirements Specification for Process-Control Systems, IEEE Transactions on Software Engineering, 20(9):684-707, 1994. Back
[MCAAI94]: Main Commission Aircraft Accident Investigation Warsaw, Report on the Accident to Airbus A320-211 Aircraft in Warsaw on 14 September 1993, Warsaw, March 1994. Text body without appendices also available from [Lad9x]. Back
[NCSA96]: NCSA, A Beginner's Guide to HTML. Available from http://www.ncsa.uiuc.edu/General/Internet/WWW/HTMLPrimer.html, 1996. Back
[OkuMatHir96]: H. Okuno, H. Matsumoto & H. Asai, TableSpec: Free Format Specification Table and Source Code Generation, Software - Practice & Experience, 26(2):213-235, 1996. Back
[Ous94]: J. K. Ousterhout, Tcl and the Tk Toolkit, Addison-Wesley, 1994. Back
[ParMadIgl94]: D. L. Parnas, J. Madey & M. Iglewski, Precise Documentation of Well-Structured Programs, IEEE Transactions on Software Engineering, 20(12):948-976, 1994. Back
[ParMad95]: D. L. Parnas & J. Madey, Functional Documents for Computer Systems, Science of Computer Programming, 25:41-61, 1995. Back
[Per84]: C. Perrow, Normal Accidents: Living With High-Risk Technologies, Basic Books, 1984. Back
[ReiMelLev95]: E. Reiter, C. Mellish & J. Levine, Automatic Generation of Technical Documentation, Applied Artificial Intelligence 9(3):259-287, 1995. Also available through http://www.dai.ed.ac.uk/daidb/staff/personal_pages/chrism/idas.html Back
[SwaBal82]: W. Swartout and R. Balzer, The Inevitable Intertwining of Specification and Implementation, Communications of the ACM, 25(7):438-440, July 1982. Back
[Thi96]: H. W. Thimbleby, Creating User Manuals for Use in Collaborative Design, ACM Conference on Computer-Human Interaction, CHI'96, Vancouver. CHI Conference Companion, M. Tauber, editor, 279-280, 1996. Back
[ThiLad95]: H. Thimbleby & P. B. Ladkin,
A Proper Explanation When You Need One,
in M. A. R. Kirby, A. J. Dix & J. E. Finlay (eds), People and
Computers X, Proceedings of the BCS Conference on HCI'95, 107-118,
Cambridge University Press, 1995.
Also available from
http://www.techfak.uni-bielefeld.de/~ladkin/
Back
[Zis72]: D. Zissos, Logic Design Algorithms, Harwell/Oxford University Press, 1972. Back
We have noted that details of the specification were omitted. This was done by enclosing the specification between HTML start and end comment tags, themselves enclosed inside meta-comment braces, as follows:
% material omitted... (this is a comment that does appear)
{<!--}
text that is processed, but does not appear in the paper
{-->}
A production system would be likely to
control such freedom of expression closely. Consider that, though
masquerading in the description above as a processed
line of text ("text that is processed..."),
in fact it was not processed.
The prototype provides a very coarse control switch. It is possible to generate a manual with either full copying of input (as in this paper) or with no copying. The former is useful for working with a specification when seeing its manual; the latter is useful for using a manual without its logic specification intruding. The switch, then, allows a single file to be used for both development/debugging and use, hence further helping to reduce errors in manuals.
| Copyright © 1999 Peter B. Ladkin, 1999-02-08 | |
|
|
by Michael Blume |