University of Tehran (IRAN)
University of Eindhoven (THE NETHERLANDS)
Performance evaluation and functional verification
for stochastic process algebras
CADP (Construction and Analysis of Distributed Processes)
Stochastic process algebras (SPAs) are mathematical formalisms for
the algebraic specification of stochastic systems. Several SPAs were
proposed, differing in the way they describe the interplay between the
stochastic and behavioural aspects of concurrent processes (keeping
the semantics of stochastic rates orthogonal or not to the behavioural
semantics, definition of communication and synchronization,
interpretation of nondeterminism). The objective of this work is to
provide a common framework enabling both performance evaluation and
functional verification for several SPAs (PEPA, MTIPP, EMPA, IMC).
The approach followed is based upon a translation from these SPAs to mCRL2, based on the definition of an intermediate common stochastic form (CSF). The approach was implemented for PEPA: using the ANTLR compiler generator, a translator from PEPA to mCRL2 was produced, which encodes PEPA processes as abstract data types and PEPA axioms as rewrite rules. Using the mCRL2 toolset, this translator generates the state spaces of PEPA descriptions. Performance evaluation is then carried out by means of a Matlab program, which takes a generated state space, produces its rate matrix (by taking the underlying Markov chain), and calculates steady-state probabilities of states based on the generated matrix. Functional verification is performed using the CADP toolbox, e.g., by model checking regular alternation-free mu-calculus formulas on the generated state space. The approach is illustrated on the PEPA model of a multichannel random access scheme similar to OFDMA.
A common framework providing performance evaluation (carried out
using Matlab) and functional verification (carried out using CADP)
for several SPAs different in nature was proposed and implemented
for PEPA. Future work concerns the implementation of translators
for other SPAs (such as EMPA and IMC) in order to integrate them
into the framework.
Hossein Hojjat, MohammadReza Mousavi, and Marjan Sirjani.
"A Framework for Performance Evaluation and Functional Verification in
Stochastic Process Algebras". In Roger L. Wainwright and Hisham Haddad,
editors, Proceedings of the 23rd Annual ACM Symposium on Applied
Computing SAC'08 (Fortaleza, Ceará, Brazil), ACM Computer
Society Press, pp. 339-346, March 2008.
Full version available on-line from http://khorshid.ece.ut.ac.ir/~hojjat/draft/sac08.pdf
or from our FTP site in PDF or PostScript
Seyyed Mohammad Reza Mousavi
HG 6.79, Dept. of Mathematics and Computer Science
Eindhoven University of Technology
P.O. Box 513, 5600MB, Eindhoven
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|