Analysing Clocked Process Algebras via Stochastic Petri Nets

Correctness and performance are two of the most important engineering issues in the devel-opment of complex software. Clocked Process Algebras (PA) such as SFSP (stochastic Finite State Processes) offer a means for systematic, hierarchical modelling of complex systems for determining both aspects of a system. SFSP is a process algebra supported by the LTSA (La-belled Transition System Analyser) tool. Traditionally, clocked PAs are solved by mapping them to Generalised Semi-Markov Processes (GSMPs) or Stochastic Timed Automata (STAs); these are then “solved ” by discrete-event simulation. This report will focus on solving clocked PAs numerically, by translating the model to a semi-Markov stochastic Petri net (SM-SPN); the net can then be solved by DNAmaca, a SM-SPN analyser that can generate and solve both Markov and semi-Markov processes in large state spaces. A translation scheme for converting SFSP into SM-SPNs is then presented. The trans-lation scheme and integration with DNAmaca has been implemented as an LTSA plug-in. This tool, which also allows for the net to be exported to be analysed with other Petri net tools such as PIPE and Medusa, will also be presented