Theory and Application of Extended Markovian Process Algebra

摘要: Many computing systems consist of a possibly huge number components that not only work independently but also communicate with each other. The catastrophic consequences failures, such as loss human lives, environmental damages, and financial losses, in many these critical compel computer scientists engineers to develop techniques for ensuring are implemented correctly despite their complexity. Although theories software tools have been developed support the formal description verification functional properties systems, recent years modeling assessment performance characteristics received attention. This thesis addresses problem providing suitable linguistic which enables designers formally describe evaluate system early stages design, order avoid cost increases due late discovery inefficiency. A reasonable solution should constitute first step towards methodology specification analysis computer, communication achieves balance among formality, expressivity, usability efficiency. As above, this we propose an integrated approach analyzing relies on extended stochastic representation time. Such approach, inspired by Olderog’s relating different views concurrent is based both stochastically timed process algebras Petri nets profit from complementary advantages: compositional modeling/manipulation capabilities structural explicit concurrency. In Markovian case, new algebra called EMPA (Extended Process Algebra), Herzog’s TIPP Hillston’s PEPA, has considerable expressive power, it allows exponentially activities immediate activities, priority probability related features, nondeterminism, intuitive master-slaves synchronization mechanism, more complex mechanisms be simulated. various phases analyses equipped collection semantics, mapping terms transition projections (functional continuous/discrete time Markov chains) generalized Ajmone Marsan-Balbo et al., respectively, well notion equivalence, describing same properties.