Institut TELECOM - TELECOM ParisTech (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
Real-time control systems, such as vehicle control systems, are often
modeled as dataflow applications taking inputs from sensors and applying
outputs to actuators. The transfer function from inputs to outputs is
refined to various functional nodes connected together. Determinism is a
fundamental property of these systems which is usually ensured by a
Although a multithreaded asynchronous approach offers better performance and extensibility, it may introduce nondeterminism. To address this issue, the authors propose abstract connectors between threads that enforce deterministic behavior of the system. These connectors, also called bridge exchangers, encapsulate the communication rules that govern thread interaction and that are derived from a protocol widely used in industry.
There are two types of connectors: the stepper deterministic bridge exchanger, connecting a high-frequency thread to a low-frequency thread, and the stagger deterministic bridge exchanger, connecting a low-frequency thread to a high-frequency thread. The connectors are integrated in the ARC (Ada to Ravenscar Converter) code generator, an Eclipse plugin that transforms real-time system architectures specified in AADL (Architecture Analysis and Design Language) into the Ravenscar Ada subset. The designer then needs only to implement the functional part of the system. This reduces programming effort as well as risk of errors.
To verify that the connectors conform to the specified protocol, the authors modeled in LOTOS the connectors and threads for six different communication configurations. Then, using CADP, an LTS (Labeled Transition System) is generated for each LOTOS specification. If the LTS does not contain a transition with a special error label, the LTS is deterministic. In case of nondeterminism, the LTS allows to exhibit an example of an execution violating the protocol rules. Finally, the authors discuss how automatic generation of LOTOS specifications of the connectors together with verification using CADP could replace costly "modified condition/decision coverage" tests for standard certification.
Real-time control systems for vehicles are typical dataflow applications
for which determinism is critical. This paper shows that an asynchronous
implementation of deterministic dataflow applications is practicable
thanks to specific connectors between threads. LOTOS and CADP were
successfully used to verify that determinism was indeed ensured by the
proposed connectors. Moreover, proof of correctness with LOTOS and CADP
is considered by the authors as an efficient possible replacement for
tests in standard certification procedures.
Irfan Hamid and Elie Najm.
"Real-time Connectors for Deterministic Data-flow". In Proceedings
of the 13th IEEE International Conference on Embedded and Real-Time
Computing Systems and Applications RTCSA'07 (Daegu, Korea),
pp. 173-182, IEEE Computer Society, August 2007
Available on-line from http://dx.doi.org/10.1109/RTCSA.2007.58
or from the CADP Web site in PDF or PostScript
Professeur - ENST
Département Informatique et Réseaux
46, rue Barrault
75634 Paris Cedex 13
Tel: + 33 (0)1 45 81 77 09
Fax: + 33 (0)1 45 81 31 19
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|