This research area involves a look at some of the philosophical and logical issues behind system correctness - what it means, for example - and system failure, which is somehow the `converse' of correctness. Reasoning about failure tells us much about what it is for a system to be correct, and aircraft accidents are amongst the most carefully investigated incidents of system failure. Consequently, the writings here are divided into some Plane Prose and Foundations. Both are treated in the book, Success and Failure of Artifacts.

The Success and Failure of Artifacts
Peter Ladkin

Abstract I study some of the philosophical and logical questions in the foundations of engineeering, such as: what is the logical situation of specification, requirements, design, software, and digital hardware, with respect to `the world' - or even with respect to each other, as components of an artifact? What can we prove mathematically, and what features stand no chance of being mathematically proven? What does it mean for a system to fail, and how do we tell? Conversely, what does it mean for a system to be `correct'? How can we explain or reason about failure? What are the features of the world that are relevant in considering these questions? What ontology do we need; what reasoning power do we need; what is the logical form of our assertions about systems? All these are natural questions to a philosophical logician, which have not in my view really begun to be answered. I offer views and arguments for these views in this series of essays, which include many of those appearing as individual reports below. (HTML)

Some Plane Prose

EMI and TWA800: Critique of a Proposal
Peter Ladkin 10 April 1998

Abstract: Elaine Scarry proposed that high intensity radio frequency fields (HIRF), possibly generated by the U.S. Military, be investigated as a possible causal factor in the TWA800 accident. Her argument appears to be very poor. I state it, and critique it. (HTML, 16K)

The Ariane 5 Accident: A Programming Problem?
Peter Ladkin 20 March 1998

Abstract: I consider three papers on the Ariane 5 first-flight accident, by Jézéquel and Meyer suggesting that the problem was one of using the appropriate system design techniques; by Garlington on the culture of flight-control and avionics software engineering; and by Baber on use of pre- and post-conditions in programming. I conclude that Jézéquel and Meyer's argument is fundamentally mistaken; and that although Garlington's (reconstructed) critique of them is broadly correct, a conclusion closer to that of Jézéquel and Meyer is most appropriate, following from a different argument from that which they gave. (HTML, 24K)

Evidence to the Transport Subcommittee on NERC/NSC, Wednesday 11 March, 1998
Peter B. Ladkin 8 March 1998

Abstract: Great Britain is building what was billed as the most advanced En-Route Air Traffic Control system in the world at the National En-Route Center (NERC) in Swanwick, Hampshire, to control traffic in the London Flight Information Region (FIR), which covers southern British airspace. The £350+ million system has run into problems, experiencing successive delivery delays. The contractor has succeeded in getting it to run on some 35 workstations but not the 200 for which it was designed. I was invited to give oral evidence before the Transport Subcommittee of the House of Commons on the issues: (a) how long would an audit of the NERC system, whose purpose would be to determine whether the current NERC system could ever be made to work, take? (b) Sir Ronald Mason's assertion that dual-sourcing, i.e. awarding the New Scottish Center contract (for the other en-route center in Britain, to cover the Scottish FIR) to another systems supplier/integrator is a `basic principle' of safety-critical system development. (HTML, 34K)

Letter to the Transport Subcommittee on NERC/NSC, Monday 17 November, 1997
Peter B. Ladkin 17 November 1997

Abstract: Great Britain is building what was billed as the most advanced En-Route Air Traffic Control system in the world at the National En-Route Center (NERC) in Swanwick, Hampshire, to control traffic in the London Flight Information Region (FIR), which covers southern British airspace. The £350+ million system has run into problems, experiencing successive delivery delays. The contractor has succeeded in getting it to run on some 35 workstations but not the 200 for which it was designed. I wrote to the Transport Subcommittee on 9 November, 1997, detailing my concern with the project, based on public evidence concerning technical problems, and with plans for its completion as briefed by National Air Traffic Services (NATS), the NERC client, in September 1997. I was briefed by specialists on the new Canadian ATC system, CAATS, and the new Australian ATC system, TAAATS, and included their comments in my letter. (HTML, 28K)

The Crash of Flight CI676, a China Airlines Airbus A300, Taipei, Taiwan, Monday 16 February, 1998: What We Know So Far
Peter B. Ladkin Latest version: 19 February 1998

Abstract: The publically-available facts concerning the accident to CI676 are given, and it is suggested where they point - and where they don't point. Specifically, they cannot show a repeat of the Nagoya accident, because of mandatory A300 system modifications since that accident. This article will be continually modified as information is gathered. (HTML, 41K)

Risks of Technological Remedy, Inside Risks, Communications of the ACM 40(11):160, Nov. 1997
Peter B. Ladkin 10 September 1997

Abstract: This guest column was invited by Peter Neumann for his Inside Risks in the November 1997 CACM. I argue by example that because of the resilience of some forms of human error, attempted technological solutions make miss the mark. The first example compares the misidentification of Flight KAL007 in 1983 with that of IR655 in 1988, and the second considers CFIT accidents, and their avoidance through GPWS and EGPWS. (HTML, 6.5K)

The Crash of Flight KE801, a Boeing B747-300, Guam, Wednesday 6 August, 1997:
What We Know So Far
Peter B. Ladkin
11 September 1997

Abstract: The publically-available facts concerning the accident to KE801 are given, along with references to sources, and the features of the accident that arise from these facts are discussed and analysed, along with various pieces of reasoning and commentary from the press. (HTML, 59K)

Analysing the 1993 Warsaw Accident With a WB-Graph
Michael Höhl and Peter B. Ladkin
8 September 1997

Abstract: We analyse the final report of the 1993 Lufthansa A320 accident in Warsaw using the WB-Graph method, and conclude that some fundamental causal factors are missing from the report's conclusions, although mentioned in the body of the report. (HTML, 30K)

Controlled Flight Into Terrain: What is Being Done?
Peter B. Ladkin
21 August 1997

Abstract: Controlled flight into terrain (CFIT) remains the greatest cause of fatalities in commercial air transportation. What is it, and what is being done to reduce its incidence? In the era of the lowest-ever aviation fatality rates, eliminating CFIT altogether poses a new challenge. (HTML, 46K)

Flying An ILS or Localiser Approach - An Example
Peter B. Ladkin
25 August 1997

Abstract: In order to understand how an aircraft flying under instrument flight rules approaches an airport for landing, one must understand standard instrument approach procedures and documentation. I introduce the procedures and charts used when flying an ILS or localiser instrument approach to an airport, as examples of a precision and non-precision approach respectively. I follow the ILS and localiser-only approaches to Won Pat International Airport in Agana, Guam. There are other traditional non-precision approach types on which I do not comment, such as VOR, VOR/DME, NDB and RNAV. There are also approach types using new-generation avionics technology which are in development but which I don't discuss: Microwave Landing System (MLS) and GPS approaches in particular. (HTML, 61K + GIF images)

Traditional Aviation Radio Navigation: An Introduction
Peter B. Ladkin
20 August 1997

Abstract: I describe the basics of aircraft land-based radio navigation with VOR and NBD reception equipment. (HTML, 39K + GIF images)

To Drive or To Fly - Is That Really The Question?
Peter B. Ladkin
24 July 1997

Abstract: Some statistical comparisons were made of fatal accidents while flying on a commercial jet and while driving on rural interstates published during 1989-1991. They largely use data from the mid 70's through the 80's, and show that the risk of dying on a commercial jet flight was uncorrelated with the length of the flight, and that for trips of longer than 303 miles, flying was safer than driving if you were in the statistical group of `safe' drivers. The age and the type of data warrant some comments on the effectiveness of statistical comparisons, in particular how commercial passenger flying may have changed in the 90's. (HTML, 36K)

Electromagnetic Interference with Aircraft Systems: why worry?
Peter B. Ladkin with colleagues
13 July 1997

Abstract: There are worries about suspected electromagnetic interference with aircraft systems from electronic devices used by passengers. Some first-hand incident reports from colleagues are included. The phenomenon seems to be hard to pin down -- colleagues explain why. It may be that the current regulatory situation affects reporting and investigation of suspected incidents. Finally, I suggest some ways in which the regulatory environment could be changed to aid investigation. (HTML)

Formalising Failure Analysis
Thorsten Gerdsmeier, Peter Ladkin and Karsten Loer
4 June 1997

Abstract: We consider systems which are artifacts designed to fulfil a goal. Most computer systems are of this sort. Criteria for success have been well-studied in the domain of specification and verification. Failure has been less well studied. The study of failure is normally exemplified by case histories. In other work, we have devised a method for determining and representing causality in case histories, called the WB-graph method. Methods need tools. We describe a tool for building and analysing WB-graphs built in DATR, a language devised for computational linguistics. (HTML)

Analysing the Cali Accident With a WB-Graph
Thorsten Gerdsmeier, Peter Ladkin and Karsten Loer
14 January 1997

Abstract: We analyse the Cali accident to American Airlines Flight 965, a Boeing 757, on 20 Dec 1995. We take the events and states from the accident report, construct a WB-graph (`Why?...Because...-graph) in both textual and graphical form of the 58 events and states, and compare this representation favorably with the Findings section of the original report. We conclude that the WB-graph is a useful structure for representing explanations of accidents. (HTML)

News and Comment on the AeroPeru B757 Accident
Peter Ladkin
8 November 1996

Abstract: Not only was this accident very disturbing: the third fatal accident to a B757 in 10 months after a 13-year perfect safety record, but news reports and statements in the early days were highly misleading. The aftermath of the Birgenair accident had sensitised me to these unfortunate social processes. The purpose of this essay is thus twofold: technically, to provide continuing timely factual information on , and some analysis of, the AeroPeru 603 accident on October 2, 1996; and, sociologically, to provide a history and commentary of what was said about the crash, when, and by whom.

Some Dubious Theses in the Tense Logic of Accidents
Peter Ladkin
27 September 1996

Abstract: Some authors propose to use forms of linear time temporal logic to describe and explain accidents. Common themes are: (1) that the 'original causes' of an accident precede all other relevant events; (2) how to pick the temporal point of view from which the accident can be explained; (3) that it is a criterion of successful explanation that an assertion of the accident event should be logically derivable from assertions of preceding causally-relevant events; (4) that the causal relation is expressed by the tense-logical 'leads to' operator. Some authors have suggested (5) that an accident is explained by exhibiting the proof of the weak fairness of the accident-action. I have explained elsewhere (ad 2) how to pick a temporal point of view, and (ad 4) that causality is not suitably expressed by 'leads to'. I show here that the other three theses are implausible; that (1) may be rescued only at great cost to intuition and common practice; that (3) may be modified in the direction of a deductive-nomological model of explanation; and that (5), if at all worthy, has a much simpler equivalent. (HTML)

Explaining Failure with Tense Logic
Peter Ladkin
10 September 1996

Abstract: Accidents involve events, and events causing other events, laid out in time until the final disaster. Boolean logic alone is insufficient to describe such failure, although its use in the shape of fault trees has been very successful. Reasoning about objects and their properties is the domain of predicate logic, and reasoning about events and their temporal relations is the province of tense logic. I show how the reasoning involved in accident analysis may be formalised in tense logic, using the past-time operator since. I also show how a fault tree may be derived from a temporal logic description without use of frame axioms. I critique proposals to use purely future operators, and to identify the causality relation with a purely temporal logic operator. Finally, I consider the important concepts of interactive consistency and tight-coupling not to be worth formalising inside a tense logic. ( HTML)

Formalism Helps in Describing Accidents
Peter Ladkin
4 September 1996

Abstract: I analyse the 'probable cause' of the 1979 Chicago DC-10 accident using a minimal formalism, and find an omission. The omission is contained in the body of the report. McDonnell Douglas's statement barely addresses the point contained in the omission. I conclude that formalism helps in accident reporting by enabling simple consistency and omission checks. (HTML)

Comments on Confusing Conversation at Cali
Dafydd Gibbon and Peter Ladkin
7 February 1996

Abstract: There are interesting linguistic aspects of the conversation between Air Traffic Control and American Airlines flight 965 shortly before the crash of AA965 near Buga, Columbia, on 20 December 1995. We discuss two features, lexical ambiguity and direction-naming conventions, as well as two linguistically incongruent features of ATC radio transmissions. (This abstract is almost longer than the article itself.)

The X-31 and A320 Warsaw Crashes: Whodunnit?
Peter Ladkin with links to others
Revised version 28 January 1996

Abstract: Recent discussions in the RISKS newsgroup asked whether there was a software or design problem involved in the crash of the X-31 research plane in January 1995. Discussants also introduced the Warsaw crash of the Airbus A320 in order to talk generally about system faults and mishaps. I proceed with an analysis of the concepts used, give my list of causal factors, and explain how I got them, and (hopefully) clarify what bits systems have, how they have problems, and whether it makes sense to blame the usual suspects for mishaps. I include information from people who really know. (HTML)

Reasons and Causes
Peter Ladkin
31 January 1996

Abstract: I discuss the art of reasoning about reasons and causes in accident investigations, in the belief that some formal understanding may improve our ability to analyse. I discuss a recent paper of Moffett, Hall, Combes, and McDermid in which they suggest a formal theory for reasoning about causes, and apply it to a partial analysis of the Lufthansa A320 accident in Warsaw. (HTML)

Also concerned with aviation are

• Analysis of a Technical Description of the Airbus A320 Braking System
• Computer-Related Incidents with Commercial Aircraft

Hazards, Risk and Incoherence
Peter Ladkin
15 June 1998

Abstract: I consider some standard engineering definitions of hazard, accident and risk, and show on a simple example how the definitions of hazard and risk are deficient. (HTML, 35K)

Abstraction and Modelling
Peter Ladkin
16 April 1997

Abstract: Engineers talk of abstractions and models. I define both, consistently with the way that engineers, computer scientists, and formal logicians use the terms. I propose that both abstractions and models have what Searle calls an agentive function, namely that both models and abstractions are models/abstractions of something, for a purpose It follows that both abstraction and modelling are most fruitfully thought of as ternary relations (or, when the purpose is forgotten, binary). A canonical example of abstraction arises in considering logical form. The criterion used to determine logical form are used mutatis mutandis to define abstraction (the purpose of logical form is given: to explicate a sentence's/proposition's role in inference; the purpose for a general abstraction remains to be selected by the abstracting agent). One may therefore consider a generalised, Wittgenstinian notion of logical form as what both abstractions and models have in common with their targets. Abstraction is closely related to the idea of describing, a relation between sentences and states of affairs; in fact it can be considered to be a precise version of description. (HTML)

Logical Form as a Binary Relation
Peter Ladkin
16 April 1997

Abstract: I consider the notion of logical form, and argue that there are considerable difficulties with defining a canonical logical form of sentences and propositions: for given A, finding a unique B such that A has the logical form of B. The purpose of logical form is unproblematically served by allowing for a given A varied B such that A has the logical form of B. I give a criterion for the relation of having the logical form of in terms of the notions of syntactic transformation and inferential equivalence. (HTML)

On Needing Models
Peter Ladkin
22 February 1996

Abstract: In his paper, Limits of Correctness in Computers, Brian Cantwell Smith proposed that program verification couldn't work, because computer systems are based on models of the `real world' and there's no general theory of how these models relate to what they're modelling. I think he's wrong, both in his arguments and his conclusions. This paper sets out my reasons.

Correctness in System Engineering
Peter Ladkin
2 April 1995

I analyse what is meant by correctness and failure of systems, using techniques from philosophical logic. I contradict a well-known claim of Fetzer. I look at the role played by specification, and simple arguments concerning failure, and try to clarify the boundary between system properties that may be proved and those that cannot be, by using two examples, one due to Boyer and Yu.
Draft Paper
HTML - Postscript - Dvi

This project aims to collect resources and reliable technical comment on aspects of computer-related commercial aviation safety on the World Wide Web. The hypertext compendium below is the result. Accidents which have a computer-related component are commented on, and where possible the text of the final report is made available. Aviation organisations concerned with safety are linked, including both administration and research. Electronic resources such as the RISKS newsgroup are consulted; opinions from experts are solicited and included. Social aspects are not given as much emphasis as technical, although many would argue they play a major role.

Computer-Related Incidents with Commercial Aircraft
Overview by Peter Ladkin with links to others
Ongoing

Abstract: There are now many commercial air transport aircraft whose primary flight controls are operated by computers, to which pilot commands and other data are input. Such aircraft are the Airbus A319/320/321/330/340 and the Boeing B777. The use of computers for such safety-critical tasks as airplane flight control is a suitable topic for computer scientists and others to consider. This is a commented Hypertext compendium of reports, papers and pertinent short observations, many from Peter Neumann's RISKS-Digest, the Forum on Risks to the Public in Computers and Related Systems, an on-line news journal which has established a reputation as the premier electronic source for news and discussion of these topics over the last ten years. I expect this page to grow continually.

This project, joint with Prof. Harold Thimbleby of Middlesex University in London, attempts to produce clear, correct, consistent and complete operating manuals for human-machine interaction tasks. Our basic point of view is that the machine-part of the task behaves as a state machine, and the human-part follows a `user manual', which consists of a procedural description of the state machine in some form or other, according to intended use. Formal specification of such interface can lead to automatic generation of operating manuals guaranteed to fulfil certain formal desiderata such as consistency and completeness. Since the quality of operating manuals in commercial aviation is widely acknowledged to be a problem, we hope this work will support the forward-generation of such manuals. The reverse-engineering of such manuals has also been addressed in one publication, the Analysis of a Technical Description of the Airbus A320 Braking System.

From Logic To Manuals Again
Harold Thimbleby and Peter Ladkin
published in IEE Proceedings - Software Engineering, June 1997

Abstract: A republication of From Logic To Manuals, below, necessitated by the manual processing of the paper at the IEE, which resulted in egregious typographical mistakes in the SEJ 11(6) (November 1996) published version, and a comment from us as to how much easier it would have been to ensure correctness had the journal worked with our HTML version that was output from the program. Ironically, the republication was marred by a mistake made by the (new) typesetters, which changed certain fonts. A corrected republication of the June 1997 IEE Proceedings on Software Engineering was sent to all subscribers. It took us almost more work to get the publishers to publish a correct version as it did to write the original paper, thus proving our point in spades -- unfortunately only to us.

From Logic To Manuals
Harold Thimbleby and Peter Ladkin
5 March 1996, revised 5 September 1996

Abstract: We demonstrate a simple language that combines specifications and manuals. This shows: first, that a 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 paper contains examples of use of the language in manual generation. It was created by running a source version (with the bulk of the text as meta-comment, and with input but no output to any examples) through the language processor. The output for the examples was automatically generated and inserted by the processor. Here are the source file and the output version with examples.

Analysis of a Technical Description of the Airbus A320 Braking System
Peter Ladkin
28 October 1994

I analyse the description of the operation of the Airbus A320 braking systems contained in the Flight Crew Operating Manual. I use the predicate-action diagrams of Lamport to express and to complete the description, and give reasons why such a more rigorous expression is preferable.
Here is a Postscript paper which appeared in High Integrity Systems 1(4), and also a short Postscript version for those who want an overview.

A proper explanation when you need one
Harold Thimbleby and Peter Ladkin
10 May 1995

Abstract: Quality program design has received considerable attention from the software engineering community. Quality user manual design has received considerable attention from the human computer interaction community. Yet manuals and systems are often independently conceived, and thus do not well complement each other. This paper shows one method of easily obtaining correct and complete user manuals guaranteed to correspond with the system they document.
Postscript - DVI
Appeared in People and Computers X, Proceedings of the BCS Conference on Human-Computer Interaction, HCI'95, ed. M. A. R. Kirby, A. J. Dix and J. E. Finlay, Cambridge University Press 1995.

I have also written essays on topical themes, discussed with others. Some such discussions are collected here.

University Education in the US, UK and Germany: A Quick Comparison
Peter Ladkin
11 December 1997

Abstract: A point-by-point comparison (somewhat superficial) of university teaching, learning, and assessment in these three countries. This précis was written as notes for an extra-curricular lecture to Bielefeld students on December 16 1997 during the demonstration concerning university reform. (HTML)

On Keeping Your Mouth Shut: Discussing Aircraft Accidents in Public
Dick Mills, Robert Dorsett and Peter Ladkin
9-12 September 1996, revised 22 October

Abstract: Dick Mills proposed in RISKS-18.42 that speculation and discussion of aircraft accidents in public as they happened had negative consequences, including continuing distress to sufferers, and suggested it should be voluntarily limited to the time after the accident report is published. Robert Dorsett cited some examples of timely discussion which, although not always accurate, had beneficial effects, and Peter Ladkin gave six reasons why he thought Mill's proposed restiction would not be beneficial. Start here.

Future University Computing Resources
Peter Ladkin
7 November 1995

Abstract: I consider what kinds of computing resources a University will be providing to students and the community. I hope that some of the ideas will have wider application than just to Universities. This is an HTML script. I'd be very glad to receive your comments.

A Debate on Social Issues with Use of the Internet
Harold Thimbleby, Peter Ladkin, Brian Randell and others
23 September 1995

Abstract: Harold Thimbleby gave a talk to the British Association for the Advancement of Science 1995 Annual Meeting on what he regards as some current unhealthy developments on the Internet. The talk got extensive coverage in the British press. Brian Randell strenuously disagreed at the talk with both Harold's presentation and his views. Brian's views did not get similar media coverage. But here on the Web, all sides get debated. Start here.

This project, joint work with Dr. Barbara Simons of IBM Santa Teresa Labs, analyses the communication of between parallel loop processes. Aims are to provide combinatorial criteria for successful parallel programs and processes - those that run without deadlock - and algorithms to serialise clusters of such processes, the important `recombination' step in parallel compilation, after decomposition and processor assignment. Work so far is collected in one monograph, which will be extended and completed in early 1997.

Static Analysis of Communicating Processes
Peter Ladkin and Barbara Simons
22 April 1995

Abstract: We define the Message Flow Graph, a graph that shows the point-to-point communications between code for concurrent processes. Trouble is, communication usually isn't point-to-point -- on different executions of the same send, the message may be received by execution of a different receive statement in the target process. For simple non-terminating processes, so-called loop processes, we show how to build a Message Flow Graph from the source code, and when one can be built. If the processes deadlock, such a graph may not be built, so our construction and associated mathematics may be used for compile-time deadlock analysis. Two mathematical conditions, the Numerical Matching Condition and the Sequence Condition are particularly important, and needed to prove the algorithm correct. We show how to perform the analysis for communications of many sorts: synchronous (rendezvous), asynchronous, and multiway synchronous - the basic analysis is performed for two-process synchronous communication and then extended.

This 139-page draft version of the manuscript does not yet include certain of our theorems on polynomial-time deadlock detection, which will be added shortly. Read it at your peril - but please tell us what you think! The monograph has been accepted for publication in the series Lecture Notes in Computer Science from Springer-Verlag.

Postscript

Static Deadlock Analysis for CSP-Type Communications
Peter Ladkin and Barbara Simons
April 1995

Abstract: We present two tests for analyzing deadlock for a class of communicating sequential processes. The tests can be used for deadlock detection in parallel and distributed programs at compile-time, or for debuggin purposes at run-time. They can also be used in conjunction with an algorithm we have for constructing valid execution traces for this class.
This paper is a resumé of Chapter 5 of the monograph for Responsive Computer Systems, ed. D.S. Fussell and M. Malek, Kluwer, 1995.

This project concerns the development and application of Lamport's TLA and the specification language TLA+. It includes both algorithm verifications, and applications such as specification and analysis of aircraft systems and joint human-machine tasks in aviation. I work with various colleagues using TLA, including Leslie Lamport of Digital Systems Research Center in Palo Alto, California and Jean-Charles Grégoire of Laboratoire INRS-Télécommunications in Montréal.

Using the Temporal Logic of Actions: A Tutorial on TLA Verification
Peter Ladkin,
17 June 1997

Abstract: This tutorial on TLA verification starts by motivating the syntax and the logic of TLA by means of a natural deduction system -- for hierarchical proofs in TLA are (inverse) natural deductions -- and works through a TLA specification and verification using the buffer example from Formal But Lively Buffers.., RVS-RR-96-07. The explanations are need-driven - TLA concepts are introduced only where necessary for working through the example - and there's a little hand-waving here and there for the same reason.
Postscript, gzip-ed, 169K - DVI, gzip-ed, 59K

Beschreibung eines vagen Echtzeit-Hybrid-Systems in TLA+
Lutz Sommerfeld, Peter Ladkin,
17 June 1997

Abstract: Diese Spezifikation beschreibt ein technischen Gerät, für das keine physikalisch oder mathematisch genaue Beschreibung vorliegt. Es liegt lediglich eine vage, zum Teil umgangssprachliche Beschreibung der Zusammenhänge vor, da die genaue Proze&slig;parameter für die Durchf&uump;hrung der Kultivierung unbekannt sind und deren Bestimmung unnötig ist. Darin unterscheidet sich die Aufgabenstellung vom ,, Steam Boiler Control Problem``. Die vorgestellte Lösung erfolgt auf einer möglichst hohen Abstraktionsebene, so da&slig; die Proze&slig;-Umwelt-Modellierung als auch doe Theorien zur logischen Form von artifacts berücksichtigt werden konnten. Als Spezifikationssprache wurde TLA+ gewählt.
Postscript

Formal but Lively Buffers in TLA+
Peter Ladkin
7 January 1996 - New Version

Abstract: I specify abstract and concrete buffers in TLA+, the specification language of Lamport's Temporal Logic of Actions, and provide a fully formal, complete proof in TLA that the one implements the other. The proof is written in Lamport's hierarchical style. The paper may be read as both a tutorial and a commentary on the use of TLA.
Postscript - DVI

The LaTeX source (200K uncompressed) could be useful as one person's view on how to write `literate proofs' in TLA using Lamport's proof style. The proof style and the additional style files which are needed to compile the LaTex source are public: Latex styles.

Accompanying the paper are copies of an older version of the proof to
depth 4: Postscript - DVI

depth 6: Postscript - DVI

depth 8: Postscript - DVI
obtained from the original using pf.sty commands, which show the higher-level structure of the proof.

Lazy Caching in TLA
Peter Ladkin, Leslie Lamport, Bryan Olivier, and Denis Roegel
18 January 1996 - Final Version

Assertional methods, formalized by TLA, are used to specify and verify the correctness of a cache coherency algorithm of Afek, Brown, and Merritt. The algorithm is described informally in

Verifying Sequential Consistent Memory Problem Definition
Rob Gerth
April 1993
Postscript

which should be read first.
Postscript - DVI - LaTeX

Lazy Cache Implements Complete Cache
Peter Ladkin
7 January 1996

The formal TLA proof that the Lazy Caching Algorithm implements a simplified algorithm called the Complete Cache, in which all caches contain entries for all memory addresses, there is no separate memory and there are no memory refresh operations. This proof is a step in proving that Lazy Caching is sequentially consistent. The choice of the invariant for the safety proof is the main issue. Other parts of the Lazy Cache proof will appear here as they become available.
Postscript - DVI

The analysis of an operating manual in
Analysis of a Technical Description of the Airbus A320 Braking System
is also accompished using TLA Predicate-Action Diagrams.

Interest is growing in the telecommunications community in the use of Message Sequence Charts (MSCs), an ITU-T standard (Z.120) language. This joint work with Prof. Stefan Leue of the University of Waterloo in Canada defines a straightforward interpretation of both `basic' MSCs and `high-level' MSCs into state machines. Various semantic problems with the MSC standard arise, which can be seen graphically (literally!) in our interpretation of MSCs into the automated verification tool Promela/XSpin from Gerard Holzmann's group at Lucent Technology's Bell Laboratories.

Implementing and Verifying Message Sequence Chart Specifications Using Promela/XSpin
Stefan Leue and Peter Ladkin
11 September 1996

Abstract: We discuss a translation of Message Sequence Charts (MSCs) into the language {\em Promela} (we call this translation an `{\em implementation}') that is consistent with the formal semantics we have previously defined for Message Flow Graphs and Message Sequence Charts, which handled the syntactic features with mathematical import from ITU-T recommendation Z.120. We report on experiments executing the Promela code using the {\em Xspin} simulator and validator. In previous work we found that potential process {\em divergence} and {\em non-local choice} situations impose problems on implementations of MSCs, and we discuss how these impact our Promela translation and suggest solutions. Finally, we show how to model-check liveness requirements imposed on MSC specifications. We use the Promela models obtained from our implementation, describe how to use control state propositions based on these models, use Linear Time Temporal Logic formulas to specify the liveness properties, and demonstrate the use of XSpin as a model checker for these properties. (compress-ed Postscript, 1.5Kb) To appear in the Proceedings of the 2nd SPIN Workshop, Rutgers, N.J., DIMACS Series, American Mathematical Society Press, 1996.

Interpreting Message Flow Graphs
Peter Ladkin and Stefan Leue
28 October 1994

Abstract: We interpret Message Flow Graphs as a finite state machines, in which states are the global states of the system. One important application of MFGs is as Message Sequence Charts, MSCs. Liveness properties of MSCs are underdefined by the Z.120 standard. We show how to compose MFGs (insofar as sense can be made of this operation without considerable qualification) and what it means, and we show how to use temporal logic to specify liveness properties precisely.
Formal Aspects of Computing 7(5):473-509
Postscript

Four Issues Concerning the Semantics of Message Flow Graphs
Peter Ladkin and Stefan Leue

Abstract: We discuss four issues concerning the semantics of Message Flow Graphs (MFGs). MFGs are extensively used as pictures of message-pasing behavior. One type of MFG, Message Sequence Chart (MSC) is ITU Standard Z.120. We require that a system described by an MFG have global states with respect to its message-passing behavior, with transitions between these states effected by atomic message-passing actions. Under this assumption, we argue (a) that the collection of global message states defined by an MFG is finite (whether for synchronous, or partially-asynchronous message-passing); (b)that the unrestricted use of `conditions' requires processes to keep control history variables of potentially unbounded size; (c) that allowing `crossing' messages of the same type implies certain properties of the environment that are neither explicit not desirable, and (d) that liveness properties of MFGs are more easily expressed by temporal logic formulas over the control states than by Büchi acceptance conditions over the same set of states.
Appeared in Formal Description Techniques VII, ed. D. Hogrefe and S. Leue, IFIP Series, Chapman and Hall, 1995.
This paper is currently being rewritten to address High-Level MSCs
[ Postscript ]

I have had ongoing interest for a decade in temporal reasoning using intervals, and in constraint satisfaction problems in general. Here are the results.

A Note on a Note on a Lemma of Ladkin
Peter Ladkin
13 September 1996, revised 14 October 1996

Abstract: Antony Galton published a recent paper correcting a Lemma of mine - well, sort of, because the Lemma was not false. However, it was useless as stated. In this note, I put the record straight(er), and offer a few comments on the social background.

Simple Reasoning With Time-Dependent Propositions
Maroua Bouzid and Peter Ladkin
4 November 1995

Simple practical reasoning with propositions whose truth values depend on time is a matter of logical engineering. Here's one approach, along with some algorithms for implementing it. We also consider reified and non-reified logics, and show that a reified logic is more appropriate than its non-reified equivalent, when time references are interpreted as union-of-convex intervals.
To appear in the Journal of the IGPL.
Postscript - DVI

Fast Algebraic Methods for Interval Constraint Problems
Peter Ladkin and Alexander Reinefeld
21 August 1996

We implement a constraint satisfaction technique for qualititive relations on intervals over dense linear orderings (sometimes called "time intervals"), and show how to solve them fast, where the bottlenecks are, and what the problem space looks like.
This is an Invited Paper for the Annals of Mathematics and Artificial Intelligence, based on a shorter paper in Springer LNCS 737, Artificial Intelligence and Symbolic Mathematical Computing, ed. Calmet and Campbell, 1993, with some new results on speed-up of the composition operation.
Postscript - DVI - LaTeX (needs prepictex.tex, pictex.tex, and postpictex.tex)

On Binary Constraint Problems
Peter Ladkin and Roger Maddux
25 January 1995

The concepts of binary constraint satisfaction problems can be naturally generalized to the relation algebras of Tarski. We do that. Among other things, we give an example of a $4$-by-$4$ matrix of infinite relations on which no iterative local path-consistency algorithm terminates; and we give a class of examples over a fixed finite algebra on which all iterative local algorithms, whether parallel or sequential, must take quadratic time. Specific relation algebras arising from interval constraint problems are also studied: the Interval Algebra, the Point Algebra, and the Containment Algebra.
Appeared in the Journal of the ACM 41(3), May 1994, 435-469.
Postscript - DVI - LaTeX (needs prepictex.tex, pictex.tex, and postpictex.tex)

An Algebraic Approach to General Boolean Constraint Problems
Hans-Werner Güsgen and Peter Ladkin
23 April 1995

The work of Ladkin and Maddux concerned binary CSPs. We show in this paper how to treat general CSPs also by algebraic logic, this time using Tarski's cylindric algebra. We formulate all the usual concepts of CSPs in this framework, including k-consistency, derived constraints, and backtrack-freeness, give an algorithm scheme for k-consistency, and prove its correctness.
Postscript - DVI

Integrating Metric and Qualitative Temporal Reasoning
Henry Kautz and Peter Ladkin
July 1991

We show how metric and Allen-style constraint networks can be integrated in a constraint-based reasoning system. We use a simple but powerful logical language for expressing both quantitative and qualitative information; develop translation algorithms between the metric and Allen sublanguages that entail minimal loss of information; and explain a constraint-propagation procedure for solving problems expressed in a combination of metric and Allen constraints.
Appeared in the Proceedings of AAAI-91 (Anaheim, CA)
MIT/AAAI Press, July 1991.
Postscript - DVI

My Thesis

The Logic of Time Representation
Peter Ladkin
November 1987

Every so often, I get requests for my thesis or for some Kestrel Institute Technical Reports on work reported in my thesis, so here it is. It includes work published in papers in AAAI-86, AAAI-87, IJCAI-87, ICSE-87 and AAAI-88 (a longer version with proofs), plus a little more. It's about 130 pages long.

Postscript - DVI

This project is joint with Laboratoire INRS-Télécommunications at the Université de Québec à Montréal. I am working primarily with Prof. Jean-Charles Grégoire on a hierarchical specification and verification of the RLP Protocol in TLA. RLP is a modified sliding-window protocol to be used in the TDMA cellular phone systems jointly being developed by Nortel, Eriksson and Nokia. A hierarchical specification is being fine-tuned and the proofs of correctness are being completed.

Pilot-controller communication is one of the most formal natural languages, designed for unambiguous and clear communication of aviation control tasks and intentions. Nevertheless, communication may go awry, as in the unfortuntate American Airlines accident of 20 December 1995 on approach to Cali, Colombia. This project, joint with Prof. Dafydd Gibbon of the University of Bielefeld Faculty of Linguistics and Literature, aims to analyse formally aspects of the language and language use, with the goal of contributing both to aviation safety and to formal linguistics. This project is in very early stages.

One result so far is
Comments on Confusing Conversation at Cali

Copyright © 1999 Peter B. Ladkin, 1999-02-08
	Last modification on 1999-06-15 by Michael Blume