Formal methods for safety-critical systems

Citation

Rudall, B.H. (2000), "Formal methods for safety-critical systems", Kybernetes, Vol. 29 No. 2. https://doi.org/10.1108/k.2000.06729baa.003

Formal methods for safety-critical systems

Keywords: Automation, Cybernetics, Research, Technological developments

Abstracts: Reports and surveys are given of selected current research and development in systems and cybernetics. They include: Interdisciplinary research, Innovations, Formal methods for safety-critical systems, Biocybernetics, Internet access for all, Management cybernetics, Cybernetics and automation, Shrinking the robot.

Formal methods for safety-critical systems

A report from the University of Glasgow, Scotland, describes how a team from its Computing Science Department has created a set of principles that can be used to guide the application of formal methods during investigations.

Recently a number of accidents have raised concerns among the public about the operation of so-called safety-critical systems. Any new techniques that can be developed to aid accident investigations will be particularly welcomed. If any sort of cybernetic feedback can be offered to the developers of such systems then we will, perhaps, all benefit.

Safety-critical systems are, by their very nature, difficult to design and are complex in operation. They are also, it would appear, difficult to define and to test, particularly if software, which is notoriously difficult to prove, is involved. Information about the operation of a safety-critical system that is the subject of an enquiry because of involvement in an accident or incident presents many challenges. Recently, as a result of accidents in the UK and in other parts of the world, there has been disquiet over the quality of the reports. An article in a Research File of IMPACT (No. 24), a publication of the UK's Engineering and Physical Sciences Research Council, confirms this. It says that:

Making sure such appalling events do not recur depends on the quality of such reports. However, because of the way reports are currently compiled, complex expert analyses may not accurately reflect the complex interactions that lead to major accidents. This can obscure the fundamental causes of an accident, and the failures that threaten safety in one application may remain uncorrected in other systems, with disastrous results.Indeed, it is perhaps surprising that few techniques can be used to analyse the interaction between system failures and human error during accident investigations.

What the research team at the University of Glasgow has done is to create a set of principles that can be used to guide the application of formal methods during investigations. The team led by Professor Chris Johnson has developed a range of computer-based tools that can enable their users to produce an overview of the argument in an accident report. The report gives an outline of the system:

Most accident reports can now be obtained electronically. The user indicates to the system what the primary conclusions were. The tool then uses information retrieval techniques to find all sections of the report (and any other associated documents) that contain evidence which relates to those conclusions: This automates the careful inspection that is traditionally performed by lawyers during the preparation of a case?

Professor Johnson says that:

Modern computing resources can cover a far larger set of documents in a fraction of the time than was previously required. My aim is not, however, to support the legal profession but to provide a tool that can be used to check the coherence of an accident report before it is published.

The Glasgow University researchers produced a simplified output from one of its case studies to illustrate how their system would react to it. The case study involved a report provided by the Australian Maritime Investigation Unit. Three levels of output were presented. A top level represented one of the conclusions of the report. A second level indicated the argument or analysis that supports the conclusion, while a final one represents the evidence to support or weaken that argument. This example, which is fully illustrated in the "Impact" article, shows how these new techniques identify usability problems in accident reports.

This research group is also using desktop virtual reality techniques to provide accident investigators, and the readers of accident reports, with the means of what they describe as "walking through" the events that have led to human error and systems failure. This is an approach that can provide a complete overview of the increasingly complex interactions that cause and exacerbate major accidents and incidents.

Any system that can provide feedback to the designers of our complex safety-critical systems is to be encouraged. Recent accidents have occurred worldwide in areas as diverse as oil and production, public order, agriculture, health care and public transport (particularly air and rail). The public's concern over the quality of the subsequent inquiries and the reports of the accidents and incidents is growing. So much so that further inquiries are demanded. It is hoped that Glasgow's Computing Science Department's new system, which sets out principles that can be used to guide the application of formal methods during an investigation, will be an important contribution to this area and at the same time ease public concern.

More information on the Web link: www-dcs.gla.ac.uk/research/gaag/summary.html