Theory and Application of Extended Markovian Process Algebra

Many computing systems consist of a possibly huge number of components that not only work independently but also communicate with each other. The catastrophic consequences of failures, such as loss of human lives, environmental damages, and financial losses, in many of these critical systems compel computer scientists and engineers to develop techniques for ensuring that these systems are implemented correctly despite of their complexity. Although a number of theories and software tools have been developed to support the formal description and verification of functional properties of systems, only in recent years the formal modeling and assessment of performance characteristics have received attention. This thesis addresses the problem of providing a suitable linguistic support which enables designers to formally describe and evaluate system performance in the early stages of system design, in order to avoid cost increases due to the late discovery of inefficiency. A reasonable solution should constitute a first step towards a methodology for the specification and analysis of computer, communication and software systems that achieves a reasonable balance among formality, expressivity, usability and efficiency. As a solution to the problem above, in this thesis we propose an integrated approach to modeling and analyzing functional and performance characteristics of systems which relies on formal description tech