SYRF
"Synchronous Reactive
Formalisms"
Esprit "Long Term Research" Project 22703
- 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
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.