Replication Features of the Splice Architecture.

Organisation:	CWI and University of Nijmegen (THE NETHERLANDS)
Method:	muCRL (micro Common Representation Language)
Tools used:	muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Coordination Architectures.
Period:	2001-2002
Size:	n/a
Description:	Splice is a distributed data space coordination architecture devised by the company Thales Nederland. It provides a coordination mechanism between loosely coupled software components (producers and consumers of data) based on a publish-subscribe paradigm. Components communicate using the Splice primitives, basically read and write operations on a distributed data space, which makes possible to add and remove components at run-time. The data space is distributed among the components, which keep their own versions of the shared space in their local storages. Each application component running on top of Splice has an associated agent responsible for handling communications. Local storages consist of triples (key, value, time stamp), each local storage containing at most one entry with a given key. Every time a data (key, value) is written by an application, the associated agent adds the current local clock value to obtain a triple (key, value, time stamp), which is forwarded asynchronously to the other components. The Splice configuration considered as a case-study consists of three types of components: Producers provide data to the rest of the system. They can be seen as abstractions of sensors (radars, thermometers, altitude measurement devices, etc.) that provide the system with an approximation of the physical reality. Transformers perform internal data computations. They can be seen as abstractions of computing devices (generation of tracks out of plots, anticipation of the future movement of objects, etc.). Consumers take data and forward it to the external environment. They can be seen as abstractions of command devices (for motors, pumps, screens, etc.). The aim of the case-study is to investigate whether replication of the transformer component (for fault-tolerance purposes) can be achieved transparently, i.e., without modifying the producer and consumer components. In order to verify replication, two versions of this system (for two input items) were specified in muCRL: the first one contains a producer, a consumer, and a transformer, and the second one contains a producer, a consumer, and two transformers. The LTSs corresponding to the two versions of the system were generated and minimized modulo branching bisimulation using the muCRL toolset, and then further minimized modulo safety equivalence using the CADP toolbox. The resulting LTSs are not safety equivalent (which is also apparent by visualizing them using CADP), meaning that the two versions of the system do not behave in the same way (the system with replicated transformer is able to duplicate some outputs). A transition sequence showing the problem was generated as diagnostic using the EVALUATOR 3.0 model-checker of CADP. Two different solutions to this problem were investigated: the first one adds logical sequence numbers to the data items, and the second one extends the read and write primitives of Splice in order to maintain the same time stamp of data values when needed. Both solutions yield equivalent LTSs, which has been checked on configurations having up to 4 and 5 input items, respectively.
Conclusions:	By making a combined use of the muCRL toolset and of the CADP toolbox, it was possible to study replication features on top of the Splice coordination architecture. This enabled to discover problems related to the use of time stamps and to propose an extension of the Splice read and write primitives with the possibility of assigning a user-defined expression to the time stamps associated to data values, leading to a more logical use of time stamps in the applications.
Publications:	[Hooman-vandePol-01] Jozef Hooman and Jaco van de Pol. "Verifying Replication on a Distributed Shared Data Space with Time Stamps". In F. Karelse, editor, Proceedings of the 2nd Progress Workshop on Embedded Systems (Veldhoven, The Netherlands), pp. 107-121. Technology Foundation (STW), Utrecht, October 2001. Available on-line at: http://www.cwi.nl/~vdpol/papers/progress_2001.ps.gz or from the CADP Web site in PDF or PostScript [Hooman-vandePol-02] Jozef Hooman and Jaco van de Pol. "Formal Verification of Replication on a Distributed Data Space Architecture". Proceedings of the 17th ACM Symposium on Applied Computing (SAC 2002), Special Track on Coordination Models, pp. 351-358, 2002. Available on-line at: http://www.cs.kun.nl/ita/publications/papers/hooman/SAC02.ps or from the CADP Web site in PDF or PostScript
Contact:	Jaco van de Pol CWI / Department of Software Engineering SEN2 (Specification and Analysis of Embedded Systems) Kruislaan 413, 1098 SJ Amsterdam, The Netherlands Room: M341 Tel: +31-(0)20-592 4137 Fax: +31-(0)20-592 4199 E-mail: Jaco.van.de.Pol@cwi.nl
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