CASPA: Symbolic Model Checking of Stochastic Systems

Conference: MMB 2006 - 13th GI/ITG Conference Measuring, Modelling and Evaluation of Computer and Communication Systems
03/27/2006 - 03/29/2006 at Nürnberg, Germany

Proceedings: MMB 2006

Pages: 4Language: englishTyp: PDF

Personal VDE Members are entitled to a 10% discount on this title

Kuntz, Matthias (Universität der Bundeswehr München, Institut für Technische Informatik)

This note describes the new features of the performance evaluation tool CASPA, which has been extended by algorithms for the model checking of stochastic systems. CASPA uses stochastic process algebras as its input language. Multi-terminal binary decision diagrams (MTBDD) are employed to represent the transition system underlying a given process algebraic specification. The specification of performability requirements can be done using a newly developed stochastic temporal logic. All phases of modelling, from model construction to model checking and numerical analysis, are based entirely on MTBDDs.