Database of Research Tools Developed Using CADP

Availability Analysis of Software Architecture Decomposition Alternatives

Organisation: Ozyegin University, Istanbul (TURKEY)
University of Twente, Enschede (THE NETHERLANDS)
European Space Agency, Noordwijk (THE NETHERLANDS)

Functionality: Software Architectures.

Tools used: FLORA
CADP (Construction and Analysis of Distributed Processes)

Period: 2016

Description: The availability of the system, that is, the percentage of time the system is up and running, heavily depends on the chosen software decomposition alternative, i.e., the way in which the software modules are grouped into recoverable units (RUs). The FLORA framework (see supports the implementation of local recovery for a particular software decomposition. Despite the support of this framework, the implementation of local recovery for a decomposition alternative is still a time-consuming and a non-trivial task. Hence, it is important to follow a systematic method to compare various alternatives and only implement the best one. A software architecture decomposition can be optimized for local recovery based on quality estimations for decomposition alternatives. However, optimization needs input from a systematic and sound method that provides availability estimations regarding decomposition alternatives at design time.

This work presents such a method, which takes as input a decomposition of the software architecture (the set of modules, the failure and repair rates for each module, and the grouping of modules into RUs). A new tool named Availability Analyzer provides an availability estimation for a given decomposition alternative based on analytical models. Once performance and availability estimations are known regarding each decomposition alternative, the Optimizer tool can select the best alternative. The selected alternative is then implemented with the FLORA framework. Availability Analyzer is implemented in Java and it makes use of the CADP toolset. It takes as input a decomposition alternative and a set of predefined MIOA specifications, which formally define the failure and recovery behavior of system modules. First, Availability Analyzer generates a set of I/O-IMC models corresponding to the given decomposition alternative. It also generates a composition script in SVL, which specifies how these models must be combined. Then, the SVL script is executed with the CADP toolset to obtain a single CTMC model by composing all the I/O-IMC models. Finally, the CTMC model is used for providing an availability estimation.

This modeling and analysis approach is illustrated on a real-life software system, namely the MPlayer open-source media player. Four different decomposition alternatives have been investigated and the availability predicted by the analytical models was compared to the availability measurements obtained from the actual implementations. It was observed that the analytical results closely match the measured availabilities.

Conclusions: The availability analysis methodology proposed follows a modular and compositional approach, which is well-established for software design but less often used for analytical purposes. In the proposed approach, separate analytical models are generated for different architectural elements. These models are composed together based on how the architectural elements are composed with each other. Different architectural configurations can be evaluated by just using (generating) a different composition script working on the same set of models. If failure behavior of a module or the recovery strategy changes, such changes should only be reflected to the corresponding analytical model that is defined separately from the other models. A CTMC model for the overall system is generated in multiple steps, thanks to the model composition and reduction features of CADP.

Publications: [Sozer-Stoelinga-Boudali-Aksit-16] Hasan Sozer, Marielle Stoelinga, Hichem Boudali, and Mehmet Aksit. "Availability Analysis of Software Architecture Decomposition Alternatives for Local Recovery". Software Quality Journal, pp. 1-27, May 2016.
Available on-line at:
or from our FTP site in PDF or PostScript
Marielle Stoelinga
Dept. of Computer Science (Zilverling)
Formal Methods and Tools group
P.O. Box 217
7500 AE Enschede
The Netherlands
Tel: +31 53 489 3773

Further remarks: This tool, amongst others, is described on the CADP Web Page:

Last modified: Wed Mar 28 11:27:35 2018.

Back to the CADP research tools page