Qualitative and Quantitative Evaluation of Stochastic Time Petri Nets

• Autorzy: Franco Cicirelli , Christian Nigro , Libero Nigro
• Języki publikacji: EN

Abstrakty

EN

Time Petri Nets (TPN) are a well-known formalism for modelling time-dependent systems with timing constraints. This paper proposes an approach based on a stochastic extension of TPN (sTPN), which enables both qualitative assessment of feasible temporal behaviors through model checking, and quantitative evaluation of a probability measure of a given behavior, by statistical model checking. The experimental work rests on the use of the latest version of the UPPAAL toolbox which supports both exhaustive non deterministic analysis and statistical model checking of system properties. The approach is demonstrated through an example.(original abstract)

Słowa kluczowe

EN

Stochastic models; Stochastic programming

PL

Modele stochastyczne; Programowanie stochastyczne

• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2015
• Tom: 5
• Strony: 763--772

Twórcy

autor

Franco Cicirelli

• Università della Calabria, Italy

autor

Christian Nigro

• Università della Calabria, Italy

autor

Libero Nigro

• Università della Calabria, Italy

Bibliografia

• E.M. Clarke, O. Grumberg, D.A. Peled, Model checking, MIT Press, 2000.
• P.M. Merlin, D.J. Farber, "Recoverability of communication protocols: implications of a theoretical study", IEEE Trans. Commun., 24(9):1036-1043, 1976.
• B. Berthomieu, M. Diaz, "Modeling and verification of time dependent systems using Time Petri Nets," IEEE Trans. Soft. Eng., Vol. 17, No. 3, pp. 259-273, Mar. 1991.
• B. Berthomieu, M. Menasche, "An enumerative approach for analyzing Time Petri Nets," Information Processing: Proc. IFIP Congress 1983, R.E.A. Mason, ed., vol. 9, pp. 41-46, 1983.
• E. Vicario, "Static analysis and dynamic steering of time dependent systems using Time Petri Nets," IEEE Trans. Soft. Eng., vol. 27, no. 8, pp. 728-748, Aug. 2001.
• R. Alur, D.L. Dill, "A theory of timed automata", Theoretical Computer Science, Vol. 126, pp. 183-235, 1994.
• B. Berthomieu, P.-O. Ribet, and F. Vernadat, "The Tool TINA- Construction of abstract state spaces for Petri Nets and Time Petri Nets," Int. J. Production Research, Vol. 42, No. 14, 2004.
• G. Bucci, L. Carnevali, L. Ridi, E. Vicario, "ORIS: a tool for modeling, verification and evaluation of real-time systems", Int. J. on Software Tools for Technology Transfer, Springer (2010) 12:391-403, DOI 10.1007/s10009-010-0156-8.
• UPPAAL on-line, www.UPPAAL.org.
• G. Behrmann, A. David, K.G. Larsen, "A tutorial on UPPAAL", In: Formal Methods for the Design of Real-Time Systems, M. Bernardo and F. Corradini Eds., Lecture Notes in Computer Science, Vol. 3185, Springer-Verlag, pp. 200-236, 2004.
• A. David, K.G. Larsen, A. Legay, M. Mikucionis, D.B. Poulsen, UPPAAL SMS Tutorial, Int. J. on Software Tools for Technology Transfer, Springer, 17:1-19, 06.01.2015, DOI 10.1007/s10009-014- 0361-y, 2015.
• M.Z. Kwiatkowska, G. Norman, D. Parker, "PRISM 4.0: Verification of Probabilistic Real-Time Systems". In Proc. of CAV 2011, pp. 585- 591, 2011.
• H.L.S. Younes, "Verification and planning for stochastic processes with asynchronous events", PhD Thesis, Carneige Mellon, 2005.
• E. Vicario, L. Sassoli, L. Carnevali, "Using stochastic state classes in quantitative evaluation of dense-time reactive systems", IEEE Trans. on Soft. Eng., Vol 35, No. 5, pp. 703-719, 2009.
• M.A. Marsan, G. Balbo, G. Conte, S. Donatelli, G. Franceschinis, Modelling with Generalized Stochastic Petri Nets, John Wiley and Sons, 2004.
• F. Cicirelli, A. Furfaro, L. Nigro, "Model checking time-dependent system specifications using time stream Petri nets and UPPAAL", Appl. Math. Comp., Vol. 218, pp. 8160-8186, 2012.
• L. Carnevali, M. Paolieri, K. Tadano, E. Vicario, "Towards the quantitative evaluation of phased maintenance procedures using non- Markovian regenerative analysis, Lecture Notes in Computer Science, Springer, Vol. 8168, pp 176-190, 2013.
• G. Bucci, A. Fedeli, L. Sassoli, and E. Vicario, "Timed state space analysis of real time preemptive systems," IEEE Trans. Soft. Eng., vol. 30, no. 2, pp. 97-111, Feb. 2004.
• F. Cicirelli, A. Furfaro, L. Nigro, F. Pupo, "Development of a schedulability analysis framework based on pTPN and UPPAAL with stopwatches". In Proc. of the 16th IEEE/ACM Int. Symp. on Distributed Simulation and Real Time Applications (DS-RT), pp. 57- 64, 2012.
• L. Carullo, A. Furfaro, L. Nigro, F. Pupo. "Modelling and Simulation of Complex Systems using TPN Designer". Simulation Modelling Practice and Theory. 11/7-8, pp. 503-532, 2003.

Identyfikatory

DOI

10.15439/2015F69