Obtaining probabilistic dynamic state graphs for TPPAL processes

Software engineers work gladly with process algebras, as they are very similar to programming languages. However, graphical models are better in order to understand how a system behaves, and even these graphical models allow us to analyze some properties of the systems. Then, in this paper we present two formalisms for the specification of concurrent systems. On the one hand we present the timed-probabilistic process algebra TPPAL, which is a suitable model for description of systems in which time and probabilities are two important factors to be considered in the description, as it occurs in real-time systems and fault-tolerant systems. Then, the specification written in TPPAL can be automatically translated into a graphical model (the so-called probabilistic dynamic state graphs), which allows us to simulate and evaluate the system. Thus, in this paper we present this translation, which is currently supported by a tool (TPAL).