Framework for Performance Evaluation and Functional Verification in Stochastic Process Algebras

Organisation:	University of Tehran (IRAN) University of Eindhoven (THE NETHERLANDS)
Functionality:	Performance evaluation and functional verification for stochastic process algebras
Tools used:	CADP (Construction and Analysis of Distributed Processes) mCRL2 Matlab
Period:	2008
Description:	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.
Conclusions:	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.
Publications:	[Hojjat-Mousavi-Sirjani-08] 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 the CADP Web site in PDF or PostScript
Contact:	Seyyed Mohammad Reza Mousavi HG 6.79, Dept. of Mathematics and Computer Science Eindhoven University of Technology P.O. Box 513, 5600MB, Eindhoven The Netherlands Tel: +31-40-247-2993 Email: m.r.mousavi@tue.nl
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page