CASPA: Symbolic Model Checking of Stochastic Systems

Konferenz: MMB 2006 - 13th GI/ITG Conference Measuring, Modelling and Evaluation of Computer and Communication Systems
27.03.2006 - 29.03.2006 in Nürnberg, Germany

Tagungsband: MMB 2006

Seiten: 4Sprache: EnglischTyp: PDF

Persönliche VDE-Mitglieder erhalten auf diesen Artikel 10% Rabatt

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.