Generating the syntactic and semantics graphs for a Markovian process algebra

JOURNAL OF COMPUTATIONAL AND APPLIED MATHEMATICS

卷:204

Article

Pelayo, Fernando L. ; Pelayo, Maria L. ; Guirao, Juan L. G.

关键词: theoretical computer science;    formal methods;    non-deterministic and probabilistic aspects;    Stochastic process algebra;    performance analysis;    real-time requirements;    design specifications;    fault tolerance;    case studies;   

DOI  :  10.1016/j.cam.2006.04.054

来源: Elsevier

【 摘 要 】

We present a couple of programs (over C and Mathematica) which allow to generate the syntactic and the semantics representations of a ROSA (Reasoning On Stochastic Algebras) process. ROSA is a Markovian process algebra for the description and analysis of probabilistic and non-deterministic concurrent processes. ROSA allows us to evaluate performance indexes as well as to check some temporal requirements. As application, we analyse the alternating bit protocol obtaining the average time to send a message, considering that channels may fail with a known probability. (C) 2006 Published by Elsevier B.V.

【 授权许可】

Free