Database of Research Tools Developed Using CADP

Performance Evaluation of Distributed Systems Based on Process Algebras

Organisation: Technical University of Eindhoven (THE NETHERLANDS)

Functionality: Performance evaluation for discrete-event systems.

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

Period: 2009

Description: This work proposes a performance evaluation framework based on process algebraic specifications and their analysis in an extended environment of the Chi toolset. First, a sound and ground-complete process algebra is provided that accommodates timed delays in a racing context. The underlying theory provides an explicit maximal progress operator and a non-trivial expansion law for the parallel composition. The algebra also provides the possibility of specifying a partial race of stochastic delays, e.g., that one delay has always a shorter, equal, or longer sample than the other delay. This is required when modeling timed systems whose correct behavior depends on the relative ordering of the timed delays, e.g., in a time dependent controller.

Second, an approach for automated performance analysis is proposed. The systems under analysis are specified using Chi, a hybrid process algebra with data. Chi specifications are translated into discrete-time probabilistic reward graphs, which comprise deterministic delays and immediate probabilistic choices. These graphs are further transformed, using either unfolding, or geometrization methods, into discrete-time Markov reward chains. Finally, the transient and long-run analysis of these chains is carried out using the BCG_TRANSIENT and BCG_STEADY tools of CADP. The approach was successfully applied for the analysis of the concurrent alternating bit protocol. The analytical results are compared with the ones obtained from discrete-event simulation and Markovian analysis using the Chi toolset on the same specification.

Conclusions: The performance evaluation framework proposed is based on a process theory that enables specification of distributed systems with discrete timed and stochastic delays. The process theory axiomatizes sequential processes comprising termination, immediate actions, and timed delays in a racing context. Performance evaluation of the process terms relies on the environment of the language Chi, which was augmented to cater for transient performance analysis by a connection to the CADP toolbox.

Publications: [Markovski-deVink-09] Jasen Markovski and Erik de Vink. "Performance Evaluation of Distributed Systems Based on a Discrete Real- and Stochastic-Time Process Algebra". Fundamenta Informaticae 95(1):157-186, 2009.
Available on-line at:
or from our FTP site in PDF or PostScript
Erik de Vink
Department of Mathematics and Computer Science
Technische Universiteit Eindhoven
P.O. Box 513
5600 MB Eindhoven
The Netherlands
Tel: +31 40 2473146
Fax: +31 40 2476685

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

Last modified: Fri Feb 19 09:13:01 2016.

Back to the CADP research tools page