5th June 2008
In this talk the formally well-rooted and extensible framework for dependability evaluation Arcade (Architectural dependability evaluation) is presented. Arcade has been designed to combine the strengths of previous approaches to the evaluation of dependability. Key features are its expressivity, its formal semantics in terms of Input/Output-Interactive Markov Chains, which enables both compositional modeling and compositional state space generation and reduction. Furthermore, the Arcade approach is extensible, hence adaptable to new circumstances or application areas. The new modeling approach is presented, its syntax and formal semantics is discussed and its applicability is illustrated by two case studies.