A MODELING TOOL FOR A NEW DEFINITION OF STOCHASTIC ACTIVITY NETWORKS

Stochastic activity networks (SANs) are a powerful and flexible extension of Petri nets. Modeling and analysis with Petri nets and their extensions need a software tool to help to construct and analyze the models. The original definition of SANs has been used as a modeling formalism in several tools. In this paper, we introduce a modeling tool called SharifSAN, which is based on a new definition of SANs. This modeling tool is useful for both the verification and performance evaluation of systems. The functional aspects of a system are verified by model checking branching temporal logic formulas, whereas its performance aspects are evaluated using some analytic and simulative methods. The nondeterministic setting of SANs is used for verification, while their stochastic setting is employed for performance evaluation. In this paper, after a brief introduction to a new definition of SANs, we introduce the SharifSAN tool and its verification and evaluation techniques. We will also present some examples of its application,