SynthesisRT: Adaptors for Real-Time Components

Organisation:	University of l'Aquila (ITALY) PopArt project-team of INRIA Grenoble - Rhône-Alpes (FRANCE)
Functionality:	Generating adaptors for real-time components
Tools used:	CADP (Construction and Analysis of Distributed Processes) TINA
Period:	2007
Description:	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.
Conclusions:	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.
Publications:	[Tivoli-Fradet-Girault-Goessler-07] 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
Contact:	Pascal Fradet Inria Rhône-Alpes, 655 av. de l'Europe, Montbonnot, 38334 Saint Ismier Cedex, France Email: Pascal.Fradet@inria.fr 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

Back to the CADP research tools page