Integrating TwoTowers and GreatSPN through a compact net semantics

Stochastic process algebras (SPAs) and stochastic Petri nets (SPNs) are two well known formal methods for the functional and performance modeling and analysis of computer, communication and software systems. Starting from the mappings from process algebras to Petri nets proposed in the literature to provide a truly concurrent semantic framework to concurrent programming languages, in this paper, we define a new SPN semantics for SPAs in order to facilitate the integration and the cross-fertilization between the two formalisms. We then prove that our net semantics is correct via a retrievability result. Afterwards, we demonstrate that it improves on the previously proposed net semantics with respect to the size of the resulting SPNs and on the standard interleaving semantics because of the detection of system symmetries. Furthermore, we illustrate its usefulness by showing how to reinterpret at the SPA level the results efficiently obtainable at the SPN level. Finally, we describe the implementation of our net semantics that has been realized to integrate the extended Markovian process algebra with generative–reactive synchronizations (EMPAgr) based software tool TwoTowers with the generalized stochastic Petri net based software tool GreatSPN.