Formal methods slowly obtained acceptance as part of the developement and analysis of complex and safety relevant systems. Mostly these methods are used to show qualitative properties of these systems (like freedom of deadlocks).

The concept of Generalized stochastic Petri nets (GSPN) is a formal description language which also shows quantitative properties as well. They enable the user to analyse performance and performability properties of the inspected system.

This talk reports on a case study where GSPN was used to show quantitative properties of a system. The object of our investigation was a component of a Fault Tolerant Computer (FTC). This component connects the FTC to an external bus system.