Bridge Exchanger Software Connectors for Dataflow Applications

Organisation:	Institut TELECOM - TELECOM ParisTech (FRANCE)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Component-based Systems.
Period:	2007
Size:	n/a
Description:	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 synchronous implementation. 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.
Conclusions:	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.
Publications:	[Hamid-Najm-07] 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
Contact:	Elie Najm Professeur - ENST Département Informatique et Réseaux 46, rue Barrault 75634 Paris Cedex 13 France Tel: + 33 (0)1 45 81 77 09 Fax: + 33 (0)1 45 81 31 19 E-mail: Elie.Najm@ENST.fr
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page