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.
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:
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.
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/
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].
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.
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.
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.
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.
******** 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 1 | Phase 2 | Phase 3 |
| Staff | ? | ? | ? |
| Travel and Subsistence | ? | ? | ? |
| Consumables | ? | ? | ? |
| Exceptional Items | ? | ? | ? |
| Equipment | ? | ? | ? |
| Indirect Costs | ? | ? | ? |
| Totals |
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.
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.
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.
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.
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
[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