Abstract
GreatSPN is a tool that supports the design and the qualitative and quantitative analysis of Generalized Stochastic Petri Nets (GSPN) and of Stochastic Well-Formed Nets (SWN). The very first version of GreatSPN saw the light in the late eighties of last century: since then two main releases where developed and widely distributed to the research community: GreatSPN1.7 [13], and GreatSPN2.0 [8]. This paper reviews the main functionalities of GreatSPN2.0 and presents some recently added features that significantly enhance the efficacy of the tool.
- M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with Generalized Stochastic Petri Nets. J. Wiley, 1995.Google Scholar
- A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model-checking continuous time Markov chains. ACM Trans. on Computational Logic, 1(1):162--170, 2000. Google ScholarDigital Library
- S. Baarir, M. Beccuti, and G. Franceschinis. New solvers for asymmetric systems in GreatSPN. In Proc. of the 5th Int. Conf. on Quantitative Eval. of Sys. (QEST08), pages 235--236, St. Malo, France, Sep. 2008. IEEE CS. Google ScholarDigital Library
- S. Baarir, C. Dutheillet, S. Haddad, and J.-M. Ilié. On the Use of Exact Lumpability in Partially Symmetrical Well-formed Nets. In Proc. of the 2nd Int. Conf. on Quantitative Evaluation of Systems (QEST05), pages 23--32, Torino, Italy, Sep. 2005. IEEE CS. Google ScholarDigital Library
- P. Ballarini, S. Bernardi, and S. Donatelli. Validation and Evaluation of a Software Solution for Fault Tolerant Distributed Synchronization. In Proc. 2002 Int. Conf. on Dependable Systems and Networks (DSN02), pages 773--784, Bethesda, MD, USA, 2002. Google ScholarDigital Library
- M. Beccuti, D. Codetta-Raiteri, G. Franceschinis, and S. Haddad. A framework to design and solve Markov Decision Well-formed Net models. In Proc. of the 4th Int. Conf. on Quantitative Eval. of Sys. (QEST07), pages 165--166, Edinburgh, UK, Sep. 2007. IEEE CS. Google ScholarDigital Library
- M. Beccuti, G. Franceschinis, S. Baarir, and J.-M. Ilié. Efficient lumpability check in partially symmetric systems. In Proc. of the 3rd Int. Conf. on the Quantitative Eval. of Sys. (QEST06), pages 211--220, Riverside, CA, USA, Sep. 2006. IEEE CS. Google ScholarDigital Library
- S. Bernardi, C. Bertoncello, S. Donatelli, G. Franceschinis, R. Gaeta, M. Gribaudo, and A. Horváth. GreatSPN in the New Millenium. In Tools, 2001 Int. Multiconf. on Measurement, Modelling and Evaluation of Computer Communication Systems, pages 17--23, 2001. TR760/2001 of the Universitat Dortmund (Germany).Google Scholar
- S. Bernardi and J. Campos. On Performance Bounds for Interval Time Petri Nets. In Proc. of the 1st International Conference on Quantitative Eval. of Sys. (QEST04), pages 50--59, Enschede, The Netherlands, Sep. 2004. IEEE CS. Google ScholarDigital Library
- S. Bernardi, S. Donatelli, and A. Horváth. Implementing compositionality for stochastic Petri nets. Software Tools for Technology Transfer, 3(4):417--430, 2001.Google ScholarCross Ref
- D. Cerotti, D. D'Aprile, S. Donatelli, and J. Sproston. Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools. In Proc. of the 6th Int. Conf. on Application of Concurrency to System Design, ACSD06, pages 143--152, Turku, Finland, June 2006. IEEE CS. Google ScholarDigital Library
- G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad. Stochastic Well-Formed Coloured Nets for Symmetric Modelling Applications. IEEE Trans. on Computers, 42(11):1343--1360, Nov. 1993. Google ScholarDigital Library
- G. Chiola, G. Franceschinis, R. Gaeta, and M. Ribaudo. GreatSPN 1.7: Graphical Editor and Analyzer for Timed and Stochastic Petri Nets. Perf. Eval., special issue on Performance Modeling Tools, 24(1&2):47--68, Nov. 1995. Google ScholarDigital Library
- S. Donatelli and P. Kemper. Integrating synchronization with priority into a Kronecker representation. Perform. Eval., 44(1-4):73--96, 2001. Google ScholarDigital Library
- G. Franceschinis, C. Bertoncello, G. Bruno, G. Vaschetti, and A. Pigozzi. SWN models of a contact center: a case study. In Proc. of the 9th Int. Workshop on Petri Nets and Performance Models (PNPM01), pages 39--48, Aachen, Germany, Sep. 2001. Google ScholarDigital Library
- M. Gribaudo, D. Codetta-Raiteri, and G. Franceschinis. Draw-Net, a customizable multi-formalism, multi-solution tool for the quantitative evaluation of systems. In Proc. of the 2nd Int. Conf. on Quantitative Eval. of Sys. (QEST05), pages 256--257, Torino, Italy, Sep. 2005. IEEE CS. Google ScholarDigital Library
- J.-M. Ilié, S. Baarir, M. Beccuti, C. Delamare, S. Donatelli, C. Dutheillet, G. Franceschinis, R. Gaeta, and P. Moreaux. Extended SWN solvers in GreatSPN. In Proc. of the 1st Int. Conf. on Quantitative Eval. of Sys. (QEST04), pages 324--325, Enschede, The Netherlands, Sep. 2004. IEEE CS. Google ScholarDigital Library
- Y. Thierry-Mieg, J.-M. Ilié, and D. Poitrenaud. A Symbolic Symbolic State Space Representation. In Proc. of the 24th Int. Conf. on Formal Techniques for Networked and Distributed Systems, pages 276--291, Madrid, Spain, Sep. 2004. LNCS 3235.Google ScholarCross Ref
- Univ. di Torino and Univ. del Piemonte Orientale. GreatSPN User's Manual , 2008. Downloadable from www.di.unito.it/~greatspn.Google Scholar
Index Terms
- The GreatSPN tool: recent enhancements
Recommendations
Stochastic modelling and evaluation using GreatSPN
GreatSPN is a tool that supports model-based (stochastic) analysis of Discrete Event Dynamic Systems (DEDS) modeled as Generalized Stochastic Petri Nets or one of its extensions like StochasticWell-formed Nets, Deterministic and Stochastic Petri Nets ...
Integrating TwoTowers and GreatSPN through a compact net semantics
Unified specification and performance evaluation using stochastic process algebrasStochastic process algebras (SPAs) and stochastic Petri nets (SPNs) are two well known formal methods for the functional and performance modeling and analysis of computer, communication and software systems. Starting from the mappings from process ...
GreatSPN 1.7: graphical editor and analyzer for timed and stochastic Petri nets
Special issue: performance modeling tools
Comments