Consortium

Summary

Proposal

Selected References

Addresses

Deliverables

Consortium

The consortium consists of full partners and associate partners. All full partners are involved in research. Associate partners submit case studies and assess the results. The project is advised by an industrial Steering Committee.

Full Partners

• Inria
  French, Research Institute, Coordinator
• Spectre project
  contact person: Nicolas Halbwachs
• Meije project
  contact person: Robert De Simone
• Ep-Atr project
  contact person: Albert Benveniste
• GMD
  German, Research Institute
  contact person: Axel Poigné
• Logikkonsult NP AB
  Swedish, Industry
  contact person: Arne Boralv
• Linköping University
  Swedish, Research Institute
  contact person: Simin Nadjm-Tehrani

Associate Partners

• Schneider-Electric (French, Industry, contact person: Daniel Perez)
• SAAB Military Aircraft (Swedish, Industry, contact person: Ove Akerlund )
• Electricité de France (French, Industry, contact person: Mazen Samaan)

Industrial Steering Committee

• Aérospatiale (France)
• Schneider-Electric (France)
• Siemens ZFE (Germany)
• Electricité de France (France)
• Thomson Multimedia, (France)
• Vérilog, (France)

Summary

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.

During the last decade, a family of new languages have been designed, mainly in France, to program such systems. These synchronous languages are based on the abstract point of view that programs instantaneously and deterministically react to input events coming from their environment. A significant amount of research has been driven around these languages, concerning their formal semantics, their compilation, their implementation on distributed architectures, and synchronous program verification.

In the meantime, synchronous programming has started to spread over in the industrial world. With the significant support of industrial users (e.g., Schneider-Electric, Aérospatiale, Dassault-Aviation, Snecma), synchronous programming environments were developed by software companies, like Verilog, Ilog, and TNI. Now, such environments are starting to be used in the large. Thanks to the EUREKA project ``SYNCHRON'' and the Esprit project ``SACRES'', the synchronous technology is now arousing a significant industrial demand from major European companies (SAAB-MA, VTT, SIEMENS, VOLVO, British-Aerospace).

The SYRF project intends to accompany these trends, and to complete these other European projects, by investigating further 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.