University of l'Aquila (ITALY)
PopArt project-team of INRIA Grenoble - Rhône-Alpes (FRANCE)
Generating adaptors for real-time components
CADP (Construction and Analysis of Distributed Processes)
Complex control systems are nowadays often designed in a modular
approach by means of libraries of building blocks. Building a
real-time system from reusable of Commercial-Off-The-Shelf
(COTS) components introduces several problems, mainly related to
compatibility, communication, and quality of service (QoS) issues.
Indeed, incompatibilities between components may arise and make
their composition impossible. This work proposes an approach to
automatically synthesize adaptors solving integration anomalies
(whenever possible) within a lightweight component model, where
components follow a data-flow interaction model. Each component is
equipped with a rich interface specifying its interaction behaviour
with the expected environment, the component clock, as well as
latency, duration, and controllability of the component's actions.
The principle of adaptor synthesis is to coordinate the interaction
behaviour of the components in order to avoid possible mismatches,
such as deadlocks.
The proposed method consists of the following steps. The input is the architectural specification of the network of components to be composed and the component interface specifications. The behavioural models of the components are generated in form of LTSs that make the elapsing of time explicit (step 1). Connected ports with different names are renamed such that complementary actions have the same label in the component LTSs. Possible mismatches/deadlocks are checked by looking for possible sink states into the parallel composition of LTSs. The adaptor synthesis process starts only if such deadlocks are detected. The synthesis first proceeds by constructing a Petri net (PN) representation of the environment expected from a component in order to avoid deadlocks (step 2). The partial views of the adaptor represented by these PNs are composed together by building causal dependencies between the reading/writing actions and by unifying time-elapsing transitions, in order to obtain an unification PN (step 3). This PN is further refined by generating its coverability graph in order to obtain the most permissive and correct adaptor (step 4). Then, by applying controller synthesis, the sinking paths and the unbounded paths are pruned from the coverability graph, yielding a Controlled Coverability Craph (CCG). If it exists, the maximal CCG generated is the LTS modeling the behaviour of the correct (i.e., deadlock-free and bounded) adaptor, which models the correct-by-construction assembly code for the components in the specified network. Steps 1, 3, and 5 are performed by the SynthesisRT tool, step 2 and the deadlock detection is carried out by CADP, and step 4 is carried out by TINA.
The approach is illustrated on the adaptor synthesis for a remote medical care system (RMCS) providing monitoring and assistance to disabled people. The RMCS is built from eight COTS components assembled into three composite components (User, Router, and Server). The deadlocks present in these composite components were automatically detected by CADP, which also exhibited deadlocking traces. TINA was used for deriving automatically the coverability graph of the unification PN of the RMCS. Then, SynthesisRT produced the adaptors for the three composite components and for their composition, yielding a correct-by-construction version of the RMCS.
The adaptor-based approach presented here allows to assemble
correct-by-construction real-time components that take into account
interaction protocols, timing information, and QoS constraints. The
approach focuses on the detection, correction, and prevention of
deadlocks and unbounded buffers due to mismatching protocols. The
work combines several techniques and formalisms (discrete controller
synthesis, clock synchronization, interface automata, PNs, and LTSs),
and builds up on tools for LTSs and PNs, such as CADP and TINA.
Massimo Tivoli, Pascal Fradet, Alain Girault, and Gregor Gössler.
"Adaptor Synthesis for Real-Time Components". In Orna Grumberg and
Michael Huth, editors, Proceedings of the 13th International
Conference on Tools and Algorithms for the Construction and Analysis
of Systems TACAS'2007 (Braga, Portugal), Lecture Notes in Computer
Science vol 4424, pp. 185-200, April 2007.
Full version available on-line from http://pop-art.inrialpes.fr/%7Efradet/PDFs/TACAS07.pdf
or from the CADP Web site in PDF or PostScript
655 av. de l'Europe, Montbonnot,
38334 Saint Ismier Cedex, France
Tel: (33) 4 76 61 52 46
Fax: (33) 4 76 61 52 52
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|