Abstract
We present a collection of tools for functional and quantitative analysis of discrete event dynamic systems (DEDS). Models can be formulated as a set of automata with synchronous communication or as Petri nets. Analysis takes place with a strong emphasis on state based analysis methods using Kronecker representations and ordered natural decision diagrams. Independent tools provide access to orthogonal techniques from different fields including computation of bisimulation equivalences, modelchecking, numerical analysis of Markov chains, and simulation. Two file formats are defined to provide a simple exchange mechanism between independent tools which allows to build various combinations of tools.
Chapter PDF
References
F. Bause, P. Buchholz, and P. Kemper. A toolbox for functional and quantitative analysis of DEDS. Forschungsbericht 680, Fachbereich Informatik, Universität Dortmund (Germany), 1998.
F. Bause, P. Kemper, and P. Kritzinger. Abstract Petri net notation. Petri Net Newsletters, 49:9–27, Oct 1995.
P. Buchholz. Numerical solution methods based on structured descriptions of Markovian models. In G. Balbo and G. Serazzi, editors, Computer Performance Evaluation-Modelling Techniques and Tools, pages 251–267. Elsevier, 1992.
P. Buchholz. Hierarchical structuring of superposed GSPNs. In Proc. 7th Int. Workshop Petri Nets and Performance Models (PNPM’97), St-Malo (France), June 1997, pages 81–90. IEEE CS Press, 1997.
P. Buchholz. An adaptive aggregation/disaggregation algorithm for hierarchical Markovian models. European Journal of Operational Research, 116(3):85–104, 1999.
P. Buchholz, G. Ciardo, S. Donatelli, and P. Kemper. Complexity of Kronecker operations on sparse matrices with applications to the solution of Markov models. Technical report, ICASE Report No. 97-66 NASA/CR-97-206274, 1997. submitted for publication.
P. Buchholz and P Kemper. Efficient computation and representation of large reachability sets for composed automata. Forschungsbericht 705, Fachbereich Informatik, Universität Dortmund (Germany), 1999.
P Buchholz and P. Kemper. Modular state level analysis of distributed systems-techniques and tool suppport. In accepted for 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’ 99), 1999.
P. Buchholz, P. Kemper, and the APNNed group. APNNed-a net editor and debugger within the APNN toolbox. In J. Desel, P. Kemper, E. Kindler, and A. Oberweis, editors, Proc. 5. Workshop Algorithmen und Werkzeuge für Petrinetze, pages 19–24. Forschungsbericht Nr. 694, FB Informatik, Universität Dortmund, Germany, 1998.
H. Hanisch, P. Kemper, and A. Lüder. A modular and compositional approach to modeling and controller verification of manufacturing systems. In accepted for 14th IFAC Word Congress, July 5-9, Beijing, China, 1999.
P. Kemper. Numerical analysis of superposed GSPNs. IEEE Trans. on Software Engineering, 22(9), Sep 1996.
P. Kemper. Reachability analysis based on structured representations. In Application and Theory of Petri Nets, LNCS 1091. Springer, 1996.
P Kemper. A mapping of autonomous net condition event systems to GSPNs. submitted for publication, 1999.
P. Kemper and R. Lübeck. Model checking based on kronecker algebra. Forschungsbericht 669, Fachbereich Informatik, Universität Dortmund (Germany), 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Buchholz, P., Kemper, P. (1999). A Toolbox for the Analysis of Discrete Event Dynamic Systems. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_41
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_41
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive