Information Systems Laboratory
Project Title: BRA-SPEC : Formal Methods and Tools for the Development of Distributed and Real-Time Systems
Funding Organization: EU - ESPRIT
Duration: 01/05/1989 - 31/03/1992
Expiration Date: 31/12/1992
Project Objective: Research into the four basic approaches to concurrency (temporal logic, automata, process algebras and assertional methods) has produced specification formalisms and associated development and verification tools that have had successful applications, but none of the formalisms completely solves the concurrency problem and all have their deficiencies. For example, temporal logic performs slendidly when proving global eventuality properties, while performing badly for local precedence properties. For automata this is exactly the other way around. The overall objective of the SPEC Action was to alleviate these deficiencies and to provide frameworks for the specification and development of distributed real-time systems that are both practically adequate and theoretically sound. So why cannot these two techniques of temporal logic and algebra be combined? In general this extends to a combination of temporal logic and algebraic techniques. Especially worthwhile has been the extension of both to real-time. Special attention is given to the development of more efficient (both in time and in space) model checking and other machine assisted verification algorithms and tools. In this respect, besides giving attention to the topics mentioned above, the aim is to extend Xesar with time and make it faster, and to extend and investigate into the possibilities of the Statechart formalism. sm.