Building Correct Reactive Systems
Description
- Project Title:
- Building Correct Reactive Systems
- Acronym:
- REACT-P
- Number:
- 6021
- Work Area:
- Theories for Concurrency and Real-Time; Specification and Verification
- Coordinator:
- Université de Liège
Grande Traverse 10
Sart Tilman
B - 4000 LIEGE
- Coordinator Country:
- B
- PARTNERS
- Universität Kiel D
IMAG F
ICS - FORTH GR
University of Uppsala S
University of Oxford Computing Laboratory UK
VTT Computer Technology Laboratory SF
- Contact Point:
- Prof. P. Wolper
- Telephone:
- +32/41-562099
- Fax:
- +32/41-562984
- E-Mail:
- pw@montefiore.ulg.ac.be
- Keywords:
- concurrency, real-time, hybrid systems, temporal logic, process algebra
- Start Date:
- 1 July 92
- Duration:
- 36 months
- Status:
- running
- Abstract:
- REACT-P addresses the problem of developing correct concurrent and reactive systems. Two complementary approaches are being considered: refinement from specification, and verification. The technical emphasis is on verification tools, the handling of realistic features of systems such as real time, and the structuring of the development process by compositionality or layering. The work builds on results achieved in SPEC (3096).
AIMS
Reactive systems continuously interact with their environment. Examples are concurrent, distributed or embedded systems. Such systems have become very widespread (eg as various forms of control systems or in computer networks), and their correctness is often critical but notably difficult to ensure. REACT-P aims to provide frameworks to help developers build correct reactive systems.
APPROACH AND METHODS
The project is based on the symbiosis between two complementary approaches of ensuring the correctness of reactive systems. The first is refinement from a specification through correctness-preserving transformations; the second is verification. The refinement approach provides a guide to the construction of the system. It is usually insufficient to guarantee correctness, since there is rarely a complete and accurate specification of the system. The system is thus specified as it is being developed. Verification provides the means to check, at various stages of the design, that the system description is actually compatible with its expected properties. These properties can range from several forms of consistency to intricate requirements specified in a logical language. Verification is thus the tool that enables the designer to be confident that the formal description of the system obtained does indeeed satisfy the requirements.
The technical emphasis of the project is threefold. First, a heavy emphasis is placed upon the verification methods that can automatically and efficiently handle real life examples. Second, a framework that incorporates the key relevant features of reactive systems is sought. For instance, real-time constraints, the behaviour of hybrid systems where the program actually controls a continuous physical device, and the probabilistic behaviour of processes, are all fully taken into account. Finally, the problem of structuring the development process by compositionality or layering is addressed. Such approaches are stepping-stones towards the use of formal design methods in large systems.
PROGRESS AND RESULTS
The first year of REACT-P has been marked by a number of achievements of which a noteworthy selection follows.
- a surprising new result that shows the decidability of verification problems for finite-state processes communicating through unbounded lossy channels has been obtained [AJ93].
- work on improving the efficiency of state-space exploration is carrying on and is giving increasingly better results, either through the use of partial-order techniques [GW93] or of abstraction.
- work on verification tools is very active with a number of partners (IMAG, Oxford, ULG) making tools widely available. a common format that will allow the combined use of a number of tools is being defined.
- the approach that was developed in spec and react for modelling timed systems and introducing in process algebras has matured and is being widely acknowledged.
- substantial progress has been made on modelling and verifying hybrid systems [KPSY92, ACH93].
- a joint case study of verification methods for lazy caching protocols has been undertaken [GE93], and an attempt to relate various techniques using prophecy variables has been undertaken [Jo93].
POTENTIAL
New insights into the development of correct reactive systems, and especially into the development of real-time and hybrid systems, are likely to be gained from this project. Verification tools that can cope with industrial examples can be expected as a downstream result.
LATEST PUBLICATIONS
- Alur R, Courcoubetis C, and Henzinger T, Computing accumulated delays in real-time systems In: Proc. 5th Workshop on Computer Aided Verification, Elounda, June 1993, Lecture Notes in Computer Science, Springer-Verlag
- Abdulla P and Jonsson B, Verifying programs with unreliable channels In: Proc. IEEE Symp. Logic in Computer Science, Montreal, Canada, June 1993
- Gerth R (Editor), Janssen W, Jonsson B, Katz S, Pnueli A, Rump C, and Zwiers J Verifying sequentially consistent memory react report, June 1993
- Godefroid P and Wolper P Using partial orders for the efficient verification of deadlock freedom and safety properties Formal Methods in System Design, 2(2):149-164, April 1993
- Jonsson B et al In search of the future: Do we need prophecy variables react report, May 1993
- Kesten Y, Pnueli A, Sifakis J, and Yovine S Integration graphs: a class of decidable hybrid systems In: Workshop on Theory of Hybrid Systems, Lyngby, Denmark, October 1992.
INFORMATION DISSEMINATION ACTIVITIES
All REACT reports and other information about the project is available by anonymous ftp from the pub/react directory on montefiore.ulg.ac.be (139.165.16.1).
Sven Müßig, last update 07-nov-1995. Your feedback is welcome.