Hossein Hojjat, MohammadReza Mousavi, Marjan Sirjani, A Framework for Performance Evaluation and Verification in Stochastic Process Algebras, Proceedings of the 22nd ACM Symposium on Applied Computing, Software Verification Track (SV'08), Fortaleza, Brazil, Vol. 1, pages 339--346, ACM Press, March 2008.
Despite its relatively short history, a wealth of formalisms exist for algebraic specification of stochastic systems. The goal of this paper is to give such formalisms a unifying framework for performance evaluation and functional verification. To this end, we propose an approach enabling a provably sound transformation from some existing stochastic process algebras, e.g., PEPA and MTIPP, to a generic form in the mCRL2 language. This way, we resolve the semantic differences among different stochastic process algebras themselves, on one hand, and between stochastic process algebras and classic ones, such as mCRL2, on the other hand. From the generic form, one can generate a state space and perform various functional and performance-related analyses, as we illustrate in this paper.
(Paper in .pdf format) (Presentation in .pdf format)Stochastic Process Algebras are process algebras in which basic action types are augmented with a stochastic delay. Such formalisms can be used for compositional performance evaluation. We have built a compiler, which translates specifications in two popular instance of SPAs, namely PEPA and MTIPP into mCRL2, a classic process algebra enhanced with Abstract Data Types (ADTs). Moreover we have implemented MATLAB tools to extract the underlying Markov chain from the mCRL2 output file and to calculate the steady state probabilities of states (with a particular incoming (or outgoing) action).
Please send your suggestions, comments or bugs concerning this tool to hojjat at sign ipm dot ir.
| The SPA2Mcrl2 Compiler is written with Java and Antlr 3.0. |
| Download from here. (Zip file containing source files and examples.) |
| A MATLAB file that parses the mCRL2 automaton output (.aut) and computes the steady states probabilities for the underlying Markov Chain. |
| Download from here. |
| A MATLAB file that parses the mCRL2 automaton output (.aut) and assigns a reward to collision states and then computes the total probability of a collision in a single channel. |
| Download from here. |
| A MATLAB file that parses the mCRL2 automaton output (.aut) and shows how the collision probability changes when the sending and response rates are changed. It can be used for making plots with e.g. surfc. In the input file of this program, the rate for req is changed to 'x' and the rate for serv is changed to 'y'. |
| Download from here. |
Last Modified: 8th June by Mohammad Mousavi