PROPOSAL

an on-line GUIDE to use the of

FORMAL METHODS

for

SAFETY-CRITICAL SYSTEMS.

Paul Trafford
draft: 1 June 1998

Introduction to the Proposal

This is a proposal for a project to disseminate information about Formal Methods, both within the research community and in industry. A case is made for a project to build on and enhance previous work carried out under Formal Methods Europe, part of Software Best Practice in the task of ESSI (European Systems and Software Initiative), within the ESPRIT Work programme of the European Union's RTD (Research and Technological Development) programme of Framework IV.

The proposed project is internet-based, supplemented by value-added summaries in the form of multimedia presentations on CD-ROM. This is designed to meet the aim of "Creating a user-friendly Information Society", the second of the four thematic programmes in the forthcoming RTD Framework.

Background to the Proposal

The internet is being used increasingly for convenient and rapid dissemination and retrieval of the latest information, whether it be for research or for development. It offers the potential for cheap and effective access to state-of-the-art technologies. Formal Methods [henceforth abbreviated as FM] is one such technology that has been recognised as offering a means for enhancing the quality of software, particularly in safety-critical applications.

At present, if a researcher is looking to determine what efforts have been made so far in his or her specialisation, then in theory the internet should offers the means to ascertain the research undertaken so far. Similarly, if a software manager is considering the use of FM for safety-critical system development, then the internet should offers the means for investigating their pertinence. We summarise briefly below the current situation in Europe regarding access to information about FM, first with regard to industry and then with regard to academia.

The main efforts for FM technology transfer have been carried out through FME:

FME: Work carried out so far

21370 FME_Guides This Esprit/ESSI Project (Guide Books and Videos for Managers on FM) has provided information on FM through Multimedia Guide Books. The videos have been shown in the Tours that were part of FMEIndSem (see the FMEInfRes Newsletters).

It recognised the "lack of easily available information about applications in which FM have been used" and offered a package consisting of Software, Seminars, Video and Audio and a few books. The project's web site showed "success stories" to emphasise their workability. Sources for the material were a range of large industrial companies (such as Philips, Alcatel, Gec-Alsthom, Ericsson, Nokia, Alenia, France-Telecom, Dassault, Aerospatiale, British-Aerospace, Rolls-Royce,...), software companies (such as SSI, IFAD, Cap-Gemini, Verilog , ..), and public users (such as RATP, Heathrow Airport, Eurocontrol, ... )

21375 FMEInfRes Its purpose has been to provide resources of information, mainly by electronic means but also through hard copy, about FM, aimed at first-time users, helping to inform them about existing experiences and available methods and technology. The resources have consisted of databases (by mid-'97 there were 85 entries in the Applications database and 59 in the Tools database), a bibliography, an electronic file of "Frequently Asked Questions" (FAQs), paper reports and a newsletter relating to FM of software development. Access to the databases, the bibliography and the FAQs has been provided by File Transfer Protocol (FTP) and World Wide Web (WWW).

21377 FMEIndSem Three tours of ten seminars were provided throughout Europe to increase the awareness of organizations developing software, of the existence, potential benefits, and state-of-the-art of FM. The seminars were well received since they taught the situations in which the application of FM is appropriate and most beneficial, describing what the benefits are.

The achievements have been highlighted in the major international FME symposiums that have taken place every 18 months: the previous couple have been in Oxford in March 1996 and in Graz, Austria in September 1997.

Other on-line Resources

1) The Formal Methods and Safety Archives at Oxford University's Computing Laboratory.

http://www.comlab.ox.ac.uk/archive/formal-methods.html

http://www.comlab.ox.ac.uk/archive/safety.html

This is in effect a huge library that lists a significant proportion of activities in the research field, including publications, conferences, people etc. In particular it has a list of introductions:

http://www.comlab.ox.ac.uk/archive/formal-methods/pubs.html#intro

2) Output from DTI/EPSRC Programme on Safety-critical Systems

http://www.augusta.co.uk/safety/

Dozens of partners participated in a project funded by the government to the tune of more than 28 million pounds sterling. The presentation is slick with useful search facilities; a natural starting point for the industrial perspective on FM in industrial software development.

3) Other Introductions

There are a range of reasonably large introductory texts. A couple (both from North America) are:

1. NASA Formal Methods Guidebooks, Volumes 1 and 2, which can be downloaded from http://eis.jpl.nasa.gov/quality/Formal_Methods/).

2. An International Survey of Industrial Applications of Formal Methods available from http://nemo.ncsl.nist.gov/ahis/formal_methods/

Current Limitations in on-line Resources

At first sight, there is a lot of information available in both cases, but closer examination reveals much inadequacy: for the researcher, technical reports and papers that cover ongoing are often not available in full on-line and, if they are, usually have to be downloaded by FTP (only an abstract is generally available for inspection). For the software manager, introductions are scattered around in various documents and it is hard to get hold of applications for given industrial scenarios. Similarly, many of these documents require FTP. The disadvantages of FTP are significant: in general, the content of these files cannot be browsed or searched on-line and do not usually make reference to on-line resources.

There are further drawbacks regarding the current resources. Although the OUCL archives offer a lot of information on FM its exploration can quickly become fragmented: the pages are just a series of indices that fail to give a flowing picture or tell a full story. On the other hand the Augusta site provides a greater feel for the engineering process, but FM features in only a few projects and there is insufficient information to gain much of a perspective. For more detailed information, reports have to be ordered by surface mail.

The FME site is organised in a more coherent fashion than OUCL and provides more FM case studies than Augusta, but still it is not possible to browse through projects on-line to gain more of a feel. The sum total of resources available is considerably less than the OUCL archive. Regarding FM_Guides, the web sites themselves convey little information and appear to have had no additions from mid '97 onwards.

Other resources, as listed in 3) are even less integrated with other information. Although the two guide books discuss issues and contain a number of case studies, it is unlikely that they will provide sufficient information on a given application area and as they are not hypertext documents, they are not likely to be updated frequently. Guide books, even of several hundred pages, have insufficient space to provide a survey that covers much more than broad issues, though they are of good quality - one in the Prentice-Hall series is exemplary among the hard back offerings [1].

An Improved Approach

A major feature that contributes to the limited availability of pertinent information is the lack of integration of efforts both in academia and industry. As part of a PhD in the use of FM for Safety-critical Systems [2], a literature survey was undertaken, from which it emerged that theoretical research generally talked about safety in abstract terms and case studies would only show how a particular selection of formalisms were utilised for particular projects. Alternative approaches to the same or similar problems were often given little credit. Further, few provided a view that integrated safety engineering and FM.

A more integrated approach was adopted in the thesis by considering a standard Safety Lifecycle (as developed by IEE and BCS) against whose structure various formal approaches could be assessed. In this way, FM was set within a wider perspective and could be more properly related to the industrial setting. Accordingly the structure could offer scope for a far-reaching and relevant literature review. The integrated approach enabled the usefulness of formal techniques to be tested in the setting of software safety engineering and conversely, safety analysis to be analysed using FM, thereby casting light on the lifecycle model.

More generally, it may be noted that mutual dependence between research and development is increasing and regarding software, the time taken for the latest research to become a product is reducing.

AIM of the PROPOSED PROJECT

The proposed project aims to make available in hypertext form more information on FM and especially to present it in a manner that is clear, consistent and useful. It may be seen as part of the long-term goal to provide hypertext information on software development - across all its stages - with the role of FM made explicit at every stage. In view of comments above, the tasks of the dissemination of the latest research and the transfer to industry will be tackled together.

This project would seek to build on the organisational structure set up by FME, but utilise the rather larger resources that may be obtained through OUCL's FM archive. This would naturally inject life to the FMEBestLib (FME Best Library) project that failed to get off the ground, yet where the potential of the OUCL resource has already been recognised. In particular, it would seek to implement some of the objectives of the FM-GUIDES project on the internet with a view to making resources more widely available and more up-to-date.

Outline of the Proposal

Two concepts are fundamental to the proposed project: context and thread. A context establishes a suitable field of application as a focus, whilst a thread builds around the context, to provide relevant step-by-step information in a continuous manner. This approach responds to the experience expressed in FMEIndSem.

So a context goes beyond general principles and concepts: a software manager inexperienced with FM may be able to establish information for a context of his or her choosing, following the threads to:


By focusing on a context, it is expected that the vast capacity of the internet will enable many case studies to be offered, thereby exceeding the bounds inherent in single printed volumes. There are many contexts which each deserve their own analysis: safety-critical systems, medical informatics, software engineering, user interfaces, communications protocols, hardware description, distributed systems, telecommunications services, quality of service, transport (railway signalling, avionics, ...) .. etc ..

This project will start with just one context by treating FM and safety-critical communication systems with the intention of scaling up later by encouraging similar treatment of other contexts. In particular, railway signalling is a prime candidate as FME has established a database on this specific area. All these contexts could be brought under one umbrella.

For the thread the aforementioned safety lifecycle model will be used, following the style in the thesis.

Implementation of the Proposal

The project would be implemented in several phases:

Phase 1 [3-6 months]:

The start of the project would be to determine an appropriate framework for development. This could begin with consideration of the PhD thesis that provides a thread from the earliest stages of requirements elicitation through to the development of a formal software model for a medical communications protocol. It is sufficiently broad in scope to be able to incorporate a significant amount of FM-related work that has been undertaken. It would be put on-line, and then expanded using extra paragraphs and numerous hyperlinks to suggest how other work fits, is complementary, or takes a different course.

Once complete, it can be made available for a certain duration to anyone with access to the internet, inviting examination and comment. A report would be presented to summarise the response so far and inviting a wider participation - which should lead to Phase 2.

Phase 2 [6 months - 1 year]:

Subsequently a group of suitably qualified individuals could meet to propose a more general framework. Once this framework is agreed upon, a team could then be appointed to build the structure and oversee its development, all the time inviting contributions. The team would work mainly in an investigative and editorial capacity - gathering and assessing relevant information, encouraging wider participation.

The project should encourage the full publication in HTML of various papers in such a way that each part is made to fit neatly into a greater whole, forming one encyclopaedia. Centres could be contacted individually and invited to contribute.

The main body of the encyclopaeadia would be hosted on a dedicated server, probably with its own domain name. The encyclopaedia can contain many threads depending upon the kind of project undertaken. Those with experience of FM can then contribute to the relevant part of the framework, either submitting / contributing chapters or sections or links to sites showing relevant work (which in turn should have links back to the super-site).

When such a repository is set up, then companies considering the development of their systems can consult the source and be able to see first of all where and how FM can relate to their project and then preferably how to gain the relevant skills. Once sufficient information is in place, then ways of navigating effectively through the material can be devised, perhaps making the site more interactive using sophisticated queries and even intelligent agents.

Phase 3 [1 year upwards]:

The on-line encyclopaeadia would be further developed.

When the project has reached sufficient maturity, the on-line resources could be supplemented by Compendiums of information, these providing enhanced value-added presentations of the on-line information, 'frozen' at particular intervals. They can be enhanced with extra resources that take too long to download, including extra software and videos. For instance, take a comparative case study - click one button to see the approach of Method 'A'; click another to see the approach of Method 'B'. Place them side by side, simulate their development cycle and compare.

They would have all the convenience of near-instant access, and be issued on a regular basis.

Costings

******** to be completed *********

Costings may be divided into the following 6 categories:

Full time: 1 initially to produce 'prototype' site, then possibly several more to research and build a consolidated site;

Part Time: several consultants to supply ongoing feedback and input; a couple of technical staff to help maintain server and databases; later, several more for Multimedia presentations.



Costing
Phase 1Phase 2 Phase 3
Staff?? ?
Travel and Subsistence? ??
Consumables?? ?
Exceptional Items?? ?
Equipment?? ?
Indirect Costs?? ?
Totals

Potential Sources of Finance

A principle of this project is that all the essential information should be available free on-line, but charges can be made for extra facilities that enhance the information.

The compendiums can be made available for a nominal charge, thus removing dependence on the internet. Once the project is established, income should be received through the compendiums, which can be increased in number and updated on a regular basis.

Another potential source of income could be adversiting - on the web site and/or on the CD-ROMs.

Participating companies would also provide some support.

Expected Benefits

For prospective users of FM, there is free access to state-of-the-art research and development which not only comes from a wide variety of sources, but is presented in such a way so that comparisons can easily be made.

For the proponents of FM, this project would promote a wider awareness and appreciation of FM in general, and publicity for contributors in particular.

Other advantages include:

1. Cheap start-up: The first phase is self-contained and all that would be required initially. It would simply enlarge the PhD and ascertain the extent to which such an idea attracts interest. This would require few individuals. Even the costs of setting up a dedicated server are relatively small.

2. Modest maintenance: in drawing on the substantive work of companies and academic centres, considerable useful work comes just from information management of already proven practices. With some extra effort (going beyond Phase 1) a significantly better framework should be developed that has input from a variety of sources.

3. If such a site receives sufficient publicity and the project starts gaining respect, then those companies and academic centres that share lots of information will gain likewise in trust and reputation. It would contribute towards greater co-operation and mutual benefit.

Conclusions

This is a good opportunity to make available the state-of-the-art techniques of FM, building on previous work in a more comprehensive and integrated manner.

Notes

Under Framework IV, the current (and last) Call for proposals (CFP) was on: 17 March 1998 were for the specific programme for research and technological development covering Specific Statistical Applications, Technologies for Components and Subsystems (TCS), High-Performance Computing and Networking (HPCN), Integration in Manufacturing (IiM). This proposal does not come under the scope of any of these.

Appendix: URL's

ENCRESS http://www.csr.ncl.ac.uk/clubs/encress.html

ESPRIT http://www.cordis.lu/esprit/home.html

CFP http://www.cordis.lu/esprit/src/call98mr.htm

ESSI http://www.cordis.lu/esprit/src/stessi.htm

FME

hub: http://www.cs.tcd.ie/FME

FM_Guides http://www.ifad.dk/projects/fmguides.html and

http://www.cybercable.tm.fr/1997/Formal/index.htm;

FMEInfRes http://www.csr.ncl.ac.uk/projects/FMEInfRes.html

FMEIndSem http://www.ifad.dk/projects/fmeindsem.html

FMEBestLib http://www.cs.tcd.ie/FME/PROJECTS/FMEBestLib.html

newsletter: http://www.cs.tcd.ie/FME/NEWSLETTER/news1.html ; ..news2.html; .. news3.html

FRAMEWORK V http://www.cordis.lu/fifth/src/cp.htm

OUCL Archives

Formal Methods: http://www.comlab.ox.ac.uk/archive/formal-methods.html

Safety: http://www.comlab.ox.ac.uk/archive/safety.html

Bibliographies

Railways Applications http://liinwww.ira.uka.de/bibliography/SE/rail.html

Other References

[1] M.G. Hinchey and J.P. Bowen (eds.). Applications of Formal Methods, Prentice Hall International Series in Computer Science, 1995. ISBN 0-13-366949-1.

http://www.comlab.ox.ac.uk/archive/formal-methods/afm-book.html

[2] Paul Trafford, The Use of Formal Methods for Safety-critical Systems, Ph.D. Thesis, Kingston University, 1997.

http://www.chezpaul.org.uk/fm/phd/index.htm