View article

Parallel systems (such as operating systems, telecommunication systems, aircraft controlling systems, banking systems, etc.) arise in many industrial applications. For applications where errors might be expensive and lead to dangerous or even catastrophal situations a precise analysis of the possible system behaviours is an important task. The quality of a parallel system depends on several properties, typically classi ed into safety properties which state that\nothing bad happens"(eg mutual exclusion, deadlock freedom or the computation of su ciently exact numerical values) and liveness or progress properties which assert that\something good will eventually happen"(eg termination, starvation freedom) OwLa82]. In realistic applications, not only the functionality of a parallel system is important, also quantitative aspects (such as time or probabilities) play a crucial role. For instance, in practice, it is useless to establish a property like\each request will eventually be answered" as there is no bound on how much time will pass between a request and the response. Typically, one aims at a property like\each request will eventually be answered within the next 5 seconds". Whether or not a property of this type can be established not only depends on the design of the system but also on the reliability of the interface with the environment or the resources that the system uses. For instance, if the response is transmitted via an uncertain medium that might loose messages a property as above can never hold. However, the cases where a physical error happens might be rare. If the failure rates are known (or can be estimated by experimental results), it makes …