Towards Reliable Computer Systems?
by Diego Latella, Stefania Gnesi and Hubert Garavel
Nowadays, society is highly dependent on computer systems and there is no doubt that in the near future complex, multimedia, computer-based systems will increasingly permeate our society and our activities, including the most critical ones. There is therefore a strongly felt need for higher quality computer systems, both from the reliability and from the performance perspectives.
The use of formal methods for the specification and verification of properties of systems is one methodological improvement of the system production process, which, together with other techniques, can make it possible to reach high quality standards. The study of formal methods for the specification, design, and analysis of distributed systems has been an important research topic over the past decade. Initially, the research in this area has concentrated on the dynamic, functional aspects of such systems, like their observable behaviour, control flow, and synchronization as properties in relative time. More recently, formal methods for the representation and analysis of functional properties in combination with quantitative aspects of system behaviour have come into focus. They allow for the specification of the delay of activities (or, actions) or the probability of actual occurrence of actions.
There is growing awareness of the importance of formal support for system development. This has reached the point that several regulatory and standards organizations are investigating ways to certify systems, in particular critical systems, and formal methods are beginning to play a major role in such activities. A direct implication of such a trend is that in the near future the use of formal methods will be part of the standard, or at least certified, development process in the computer industry. This is true in particular for those industries developing complex systems – such as multimedia and telecommunications –and safety critical systems.
In order to be more directly applicable, formal specification and verification techniques and tools must reach a high level of usability in the near future. These were the underlying motivations which led to the setting up, in March 1996, of the ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS).
The main objectives of the Working Group are:
• to bring together scientists mainly, but not only, from institutions within ERCIM, who are active in the field of formal methods and are willing to exchange their experience in the industrial usage of such methods
• to coordinate efforts in the transfer of the formal methods technology and knowledge to the industry
• to promote research and development for the improvement of formal methods and tools with respect to their usage in industry.
The above objectives have been pursued by means of a series of workshops and publications, by initiation of joint projects between ERCIM sites and by the ERCIM Fellowship Programme. Since 1996, four international workshops have been held (Oxford, 1996; Cesena, 1997; Amsterdam, 1998; and Trento, 1999). Additionally, four special issues in international scientific journals have been published.
As regards industrial collaborations, the members of the Working Group are particularly active. Examples of industrial applications are:
• verification of a surge storm barrier control system for Rotterdam
• verification of railway interlocking systems
• verification and test generation for high-end multiprocessor architectures
• specification and test generation for a telecom Corba platform
• automatic test generation for OSEK protocols in automotive systems
• interoperability testing of ISDN networks
• verification of telecom programs written in Erlang
• performance evaluation of an Internet audio tool
• proof-carrying code for Java Virtual Machines focusing on confidentiality properties of mobile code
• secure micro-payment on the Web only to mention a few.
From 1996 to 1999, the Working Group has been founded and coordinated by Diego Latella (CNUCE-CNR, Italy) and Stefania Gnesi (IEI-CNR, Italy). Since July 1999, the Working Group coordinator is Hubert Garavel from INRIA Rhone-Alpes.
Links:
FMICS Web site: http://www.inrialpes.fr/vasy/fmics
Please contact:
Hubert Garavel - INRIA
Tel: +33 4 76 61 52 24
E-mail: hubert.garavel@inria.fr
