Abstract:

An integrated approach for modeling and analyzing functional and performance properties of concurrent systems is proposed, which is based on Extended Markovian Process Algebra (EMPA) and Generalized Stochastic Petri Nets (GSPNs). EMPA is a process algebra where each action is a pair composed of the type, which expresses the functionality of the action, and the rate, which expresses the duration of the action. EMPA is introduced together with its integrated interleaving semantics (a transition system labeled on both action types and action rates), its functional semantics (a transition system labeled on action types only), its performance semantics (a homogeneous continuous-time Markov chain), and its integrated truly concurrent semantics (a GSPN). Finally, the case study of the alternating bit protocol is presented in order to illustrate the integrated approach as well as the expressive power of EMPA.