Inria Sophia-Antipolis - Méditerranée / OASIS project-team (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
931,640,080 states and 16,435,355,306 transitions
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.
Regarding the usage of CADP for analyzing large systems,
[Gaspar-Henrio-Madelaine-13] states the following:
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
Inria / OASIS project-team
2004, route des Lucioles
F-06902 Sophia Antipolis
Tel: +33 (0)4 92 38 71 64
Fax: +33 (0)4 92 38 76 44
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|