Michael Günther
ABSTRACT
CASPA is a stochastic process algebra tool for performance and dependability modelling, analysis and verification. It is based entirely on the symbolic data structure MTBDD (multi-terminal binary decision diagram) which enables the tool to handle models with very large state space. This paper describes an extension of CASPA's solving engine for path-based analysis. We present a symbolic variant of the k-shortest-path algorithm of Azevedo, which works in conjunction with a symbolic variant of Dijkstra's shortest path algorithm. A non-trivial case study illustrates the use of this kind of path-based analysis.
- J. Azevedo, J. Madeira, E. Martins, and F. Pires. A Shortest Paths Ranking Algorithm. In Proc. of the Annual Conference AIRO'90 Operational Research Society of Italy, pages 1001--1011, IEEE, 1990.Google Scholar
- J. Bachmann, M. Riedl, J. Schuster, and M. Siegle. An Efficient Symbolic Elimination Algorithm for the Stochastic Process Algebra tool CASPA. In SOFSEM 2009: Theory and Practice of Computer Science, pages 485--496, Špindlerův Mlýn, Czech Republic, 2009. Springer, LNCS 5404. Google ScholarDigital Library
- M. Bouissou and J.-L. Bon. A new formalism that combines advantages of fault-trees and Markov models: Boolean logic driven Markov processes. Reliability Engineering and System Safety, 82:149--163, 2003.Google ScholarCross Ref
- CUDD website. http://vlsi.colorado.edu/~fabio/CUDD/, (last checked March 2010).Google Scholar
- M. Günther. Pfadbasierte Algorithmen zur Zuverlässigkeitsanalyse. Master's thesis, Univ. der Bundeswehr München, Fakultät für Informatik (in German), 2009.Google Scholar
- M. Kuntz, M. Siegle, and E. Werner. Symbolic Performance and Dependability Evaluation with the Tool CASPA. In Europ. Perf. Engineering Workshop, pages 293--307. LNCS 3236, 2004.Google Scholar
- W. Schmid. Berechnung kürzester Wege in Straßennetzen mit Wegeverboten. PhD thesis, Universität Stuttgart, Fakultät für Bauingenieur- und Vermessungswesen, 2000.Google Scholar
- M. Siegle. Behaviour analysis of communication systems: Compositional modelling, compact representation and analysis of performability properties. Shaker Verlag, Aachen, 2002.Google Scholar
- M. Walter, M. Siegle, and A. Bode. OpenSESAME: The Simple but Extensive, Structured Availability Modeling Environment. Reliability Engineering and System Safety, 93(6):857--873, 2007.Google ScholarCross Ref
- E. Werner. Leistungsbewertung mit Multi-terminalen Binären Entscheidungsdiagrammen. Master's thesis, Univ. Erlangen, Computer Science 7 (in German), 2003.Google Scholar
Recommendations
An Efficient Symbolic Elimination Algorithm for the Stochastic Process Algebra Tool CASPA
SOFSEM '09: Proceedings of the 35th Conference on Current Trends in Theory and Practice of Computer ScienceCASPA is a stochastic process algebra tool for performance and dependability modelling, analysis and verification. It is based entirely on the symbolic data structure MTBDD (multi-terminal binary decision diagram) which enables the tool to handle models ...
Dependability modelling with the stochastic process algebra tool CASPA
DYADEM-FTS '10: Proceedings of the First Workshop on DYnamic Aspects in DEpendability Models for Fault-Tolerant SystemsThis note describes CASPA, a stochastic process algebra tool for performance and dependability modelling, analysis and verification. Internally, the tool works with the symbolic data structure MTBDD (multi-terminal binary decision diagram), which allows ...
Near-shortest and K-shortest simple paths
We present a new algorithm for enumerating all near-shortest simple (loopless) s-t paths in a graph G = (V, E) with nonnegative edge lengths. Letting n = |V| and m = |E|, the time per path enumerated is O(nS(n, m)) given a user-selected shortest-path ...
Comments