A new GreatSPN GUI for GSPN editing and CSLTA model checking

Abstract

This tool demonstration paper describes a new Graphical User Interface for the interactive modeling and verification of GSPN systems with the stochastic logic CSLTA. The GUI provides a modern and fully-featured environment designed around a complete modeling workflow: The user designs a GSPN model, a DTA (automaton describing properties for the CSLTA logic), and can simulate the GSPN behavior and the model checking process with an interactive simulation (a sort of "joint token game"). The tool then supports CSLTA model-checking and the computation of classical performance indices and qualitative properties. The aim is to provide a state-of-the-art integrated environment for the quantitative and qualitative analysis of GSPNs with the support of GreatSPN solvers and of the MC4CSLTA model checker. © 2014 Springer International Publishing.