SPLICE Coordination Architecture.

Organisation:	Hollandse SignaalApparaten B.V. and CWI Amsterdam (THE NETHERLANDS)
Method:	muCRL
Tools used:	muCRL toolset (micro Common Representation Language) CADP (Construction and Analysis of Distributed Processes)
Domain:	Communication Protocols.
Period:	2000
Size:	about 1600 lines of muCRL about 4.5 millions of states
Description:	The software architecture SPLICE (Subscription Paradigm for the Logical Interconnection of Concurrent Engines) is used by Hollandse Signaalapparaten to build distributed control systems. SPLICE enables the construction of complex systems based on highly independent application processes that together form a consistent and coherent mechanism. A SPLICE system consists of a number of autonomous applications, each of which communicates with the rest of the system by its local agent, which is connected to the other agents by a communication network. The SPLICE architecture provides a shared database to which every agent can have access by means of publications and subscriptions broadcasted over the network. A specification of SPLICE has been developed using the muCRL language. The specification covers the coordination features of SPLICE (i.e., the API allowing clients to coordinate their behaviour by having access to one shared data model). The SPLICE model considered assumes that the hardware and network are fault-free, and concentrates on the external behaviour rather than internal behaviour of the architecture. Finally, the temporal aspects have not been considered, since the muCRL toolset does not yet support the temporal features present in the specification language. The muCRL specification also contains a limited model of Ethernet (CSMA/CD protocol). Several properties of the SPLICE architecture have been identified and formulated in regular alternation-free mu-calculus, which is the property specification language accepted as input by the EVALUATOR model-checker of CADP. The properties express conditional deadlock freedom (absence of deadlock in normal circumstances, i.e., when no hardware failure has occurred and the system has not terminated), soundness (all data read has been written), and weak completeness (for any data written, there are not only failing read actions until the data is overwritten). The verification has been successfully performed for a total of 6 scenarios, each consisting of two SPLICE clients. The underlying transition systems have been generated using the muCRL toolset and the correctness properties have been checked on these models using the EVALUATOR tool.
Conclusions:	A detailed formal model of the SPLICE architecture has been developed using the muCRL specification language, and several correctness properties of SPLICE have been identified and expressed in temporal logic. These specifications provide formal, unambigous descriptions of SPLICE, and therefore constitute a useful complement to the informal specifications of the architecture. By a combined use of the muCRL and CADP toolsets, the correctness properties have been successfully verified on several behaviour scenarios of SPLICE applications, thus contributing to increase the confidence in the good functioning of the architecture.
Publications:	[Dechering-Langevelde-00-a] P.F.G. Dechering and I.A. van Langevelde. "Towards Automated Verification of Splice in muCRL". Technical Report SEN-R0015, CWI, Amsterdam, May 2000. Available on-line at: http://www.cwi.nl/static/publications/reports/abs/SEN-R0015.html or from the CADP Web site in PDF or PostScript [Dechering-Langevelde-00-b] P.F.G. Dechering and I.A. van Langevelde. "On the Verification of Coordination". In A. Porto and G-C. Roman, editors, Proceedings of the 4th International Conference on Coordination Models and Languages (Limassol, Cyprus), LNCS vol. 1906, pp. 335-340, Springer-Verlag, September 2000. Available on-line at: ftp://ftp.cwi.nl/pub/izak/papers/coordination00.pdf or from the CADP Web site in PDF or PostScript
Contact:	Izak van Langevelde CWI / SEN2 P.O. Box 94079 NL-1090 GB Amsterdam The Netherlands Tel: (+31) 20 592 4165 E-mail: Izak.van.Langevelde@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