Hypermanager for Reconfigurable Component-Based Systems

Organisation:	Inria Sophia-Antipolis - Méditerranée / OASIS project-team (FRANCE) ActiveEon
Method:	GCM/Proactive pNets Fiacre FLAC CADP (Construction and Analysis of Distributed Processes)
Domain:	Component-based Systems
Period:	2013
Size:	931,640,080 states and 16,435,355,306 transitions
Description:	Nowadays applications are expected to be full-featured, performant, and reliable. Moreover, for distributed applications high-availability is also cause of concern. Taming this complexity makes the use of modular techniques mandatory. To this end, the modularity offered by component-based systems made it one of the most employed paradigms in software engineering. Embracing this approach enables structural specifications, thus leveraging formal verification. This gains special relevance for reconfigurable component-based systems. Indeed, while offering systems with an higher availability, the ability to evolve at runtime inherently increases the complexity of an application, making its formal verification a challenging task. This case-study was carried out in the context of the Spinnaker collaborative project, which aims at contributing to the widespread adoption of RFID-based technology. To this end, the contribution comes with the design and implementation of a non-intrusive, flexible, and reliable solution that can integrate itself with other already deployed systems. This solution is a HyperManager, a general purpose monitoring application with autonomic features. The goal was to deliver a modular solution that would be capable of monitoring a distributed application and react to certain events. As such, the HyperManager is itself a distributed application, deployed alongside the target application to monitor. It was built using GCM/ProActive, a Java middleware for parallel and distributed programming that follows the principles of the GCM component model. For the purposes of this project, it had the goal to monitor the E-Connectware (ECW) framework in a loosely coupled manner. The HyperManager was modeled formally using pNets, which required to provide a behaviour for each service method. This was done by considering a user-version LTS for all of them (by omitting all the machinery involving futures and proxies). The behavioural models are built by encoding the involved processes in the Fiacre specification language. Then, the FLAC compiler translates the Fiacre specification to LOTOS, on which the CADP toolbox is used for analysis. LTSs are generated in a distributed manner using BCG_OPEN and DISTRIBUTOR, and then minimized using BCG_MIN. The intermediate operations (LTS replication, hiding, synchronous products) are automated using SVL scripts. At last, seven correctness properties were specified in MCL and successfully verified using the EVALUATOR 4.0 model checking.
Conclusions:	Regarding the usage of CADP for analyzing large systems, [Gaspar-Henrio-Madelaine-13] states the following: As usual in the realm of formal verification, abstraction is the key. Taking advantage of CADP's facilities for communication hiding, one can specify actions that need not to be observed for verification purposes, which further enhances the effects of posteriori minimization by branching bisimulation. This illustrates the pragmatic rationale of formal verification by model checking - the most likely reason behind its broad acceptance in the industry.
Publications:	[Gaspar-Henrio-Madelaine-13] Nuno Gaspar, Ludovic Henrio, and Eric Madelaine. Formally Reasoning on a Reconfigurable Component-Based System - A Case Study for the Industrial World. Proceedings of the 10th International Symposium on Formal Aspects of Component Software FACS'13 (Nanchang, China), October 2013. Available on-line at: http://www-sop.inria.fr/members/Nuno.Gaspar/files/hypermanager/paper.pdf or from the CADP Web site in PDF and PostScript
Contact:	Ludovic Henrio Inria / OASIS project-team 2004, route des Lucioles BP 93 F-06902 Sophia Antipolis France Tel: +33 (0)4 92 38 71 64 Fax: +33 (0)4 92 38 76 44 Email: ludovic.henrio@cnrs.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