Esprit "Long Term Research" Project 22703, 1996-1999

Embedded, safety critical computer systems are of growing importance in our everyday life. They are often called ``reactive systems’’ in the literature, since their role is to react to events coming from their physical environment. Embedded control systems for aircraft, railways, or even cars, are well-known examples of reactive systems. Most plants now involve complex reactive systems for monitoring and supervision. Communication protocols or man-machine interfaces are also reactive systems. It is widely recognised that these systems are those whose reliability is the most critical, as design or implementation errors can have disastrous consequences. Therefore, there is a crucial need, in this domain, for clean description formalisms, design and implementation methods and tools, and formal verification.



The SYRF project intends to investigate some long time research tracks:

— Combination of formalisms: The different synchronous formalisms rely on different programming paradigms, such as being imperative or declarative, and address different aspects of applications, e.g., discrete change of state or continuous change of state. There is a strong requirement stated by users freely to merge the different formalisms to support different types of subtasks by the most adequate formalism.
— Program verification: Although realistic industrial experiences have been successfully conducted, program verification techniques must be extended, in particular to encompass symbolic techniques and to handle properties depending on the behaviour of numerical variables. Methodological aspects must be developed too.
— Code distribution and multi-tasking: At the implementation level, available industrial compilers only produce standard sequential code. Other implementations must be studied, concerning distributed code generation, and integration with real-time operating systems offering multitasking. Generic techniques and methods for different targets must be developed.
— Integrating synchrony and asynchrony: In general, synchronous programs must be integrated in a complex, asynchronous environment. There is strong need for models integrating synchronous and asynchronous features, while offering a global view of the system, preserving a clean formal semantics, and allowing formal verification at the global level.
— Connection with hardware/software codesign: Synchronous languages are suitable for compilation not only into software, but also into hardware (synchronous circuits) as well. While not sufficient in itself for tackling most interesting issues in hardware/software codesign (a quite important goal in reactive system design, nowadays), this still makes synchronous languages a promising starting point for powerful description formalisms with firm semantics and further expressive capabilities in this direction.
— Integration of analog and discrete synchronous design: In many cases, design methods should be based on an approach going from analog/continuous to discrete systems, since the physical environment of the system must be taken into account.


— VERIMAG (coordinator)
— Inria
— Logikkonsult NP AB
— Linköping University
— Schneider-Electric
— SAAB Military Aircraft
— Electricité de France

View online : Official Project page