Abstract :
We present a framework for specification and verification of real-time and reliability in distributed systems. The framework consists of a language for describing the operational behaviour of systems, a logic for formulating system properties, and an algorithm for verifying that descriptions an the language satisfy formulas expressed in the logic. The language, TPCCS, as an extension of Miher??s Calculus of Communicating Systems (CCS) with discrete tame and probabilities. The logic, TPCTL, is a branching time temporal logic, essentially extending Emerson, Clarke and Sistla??s CTL with quantitative time and probabilities. The logic can be used to formulate reliability, real-time, and performance properties. A small example is used to illustrate how the operational behaviour of a system can be formulated in TPCCS, how its properties can be specified in TPCTL, and how we can verify that the TPCCS description satisfies the specified properties.
