Abstract
Modelling and analysis of time-dependent concurrent/distributed systems is very challenging when such systems also exhibit a stochastic behavior. In this paper, the partially stochastic Time Petri Net formalism (psTPN) is introduced, which has the expressive power to model realistic complex systems. Each transition owns both a non-deterministic temporal interval and a stochastic duration established by a generally distributed (i.e., not necessarily Markovian) probabilistic function whose samples are constrained to occur in the associated time interval. A psTPN model admits two possible interpretations: the non-deterministic (which ignores stochastic aspects), useful for qualitative analysis (establishing that an event can possibly occur) and the stochastic one (which considers stochastic behavior), useful for quantitative analysis (estimating the probability for an event to actually occur). The paper focuses on the reduction of psTPN onto Uppaal timed automata which permit non-deterministic analysis through the symbolic exhaustive model checker, and quantitative analysis through the statistical model checker (SMC) which rests on simulations and statistical inference. Although potentially less accurate of analysis techniques based on numerical methods and stochastic state space enumeration, this paper claims that statistical model checking can provide quantitative property assessment which is of practical engineering value. As an example, psTPN is exploited in the paper to model and evaluate a stochastic version of the Fisher timed-based mutual exclusion algorithm.
C. Nigro—Independent Computing Professional, Italy.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H.: Performance analysis of distributed and asynchronous systems using probabilistic timed actors. AVoCS 2014, The Netherlands (2014)
Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H., Cimini, M.: PTRebeca: modeling and analysis of distributed and asynchronous systems. Sci. Comput. Program. 128, 22–50 (2016)
Paolieri, M., Horváth, A., Vicario, E.: Probabilistic model checking of regenerative concurrent systems. IEEE Trans. Soft. Eng. 42, 153–169 (2016)
Horvath, A., Paolieri, M., Ridi, L., Vicario, V.: Probabilistic model checking of non-Markovian models with generally distributed timers. In: Quantitative Evaluation of Systems (QEST) (2011)
Nigro, L., Sciammarella, P.F.: Qualitative and quantitative model checking of distributed probabilistic timed actors. Simul. Model. Pract. Theory 87, 343–368 (2018)
Jafari, A., Khamespanah, E., Kristinsson, H., Sirjani, M., Magnusson, B.: Statistical model checking of timed Rebeca models. Comput. Lang. Syst. Struct. 45, 53–79 (2016). https://doi.org/10.1016/j.cl.2016.01.004
Merlin, P.M., Farber, D.J.: Recoverability of communication protocols: implications of a theoretical study. IEEE Trans. Commun. 24(9), 1036–1043 (1976)
Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using Time Petri Nets. IEEE Trans. Soft. Eng. 17(3), 259–273 (1991)
Carnevali, L., Paolieri, M., Tadano, K., Vicario, E.: Towards the quantitative evaluation of phased maintenance procedures using non-Markovian regenerative analysis. Lect. Notes Comput. Sci. Springer 8168, 176–190 (2013)
Younes, H.L.S., Kwiatkowska, M., Normaln, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transf. 8(3), 216–228 (2006)
Vicario, E., Sassoli, L., Carnevali, L.: Using stochastic state classes in quantitative evaluation of dense-time reactive systems. IEEE Trans. Soft. Eng. 35(5), 703–719 (2009)
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems. Lecture Notes in Computer Science (LNCS), vol. 3185, pp. 200–236. Springer-Verlag, Berlin (2004)
David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transfer 17, 1–19 (2015). Springer, updated on 26 January 2018, www.it.uu.se/research/group/darts/papers/texts/uppaal-smc-tutorial.pdf
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Agha, A., Palmskog, K.A.: Survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1–6:39 (2018). http://doi.acm.org/10.1145/3158668
Gafni, E., Mitzenmaker, M.: Analysis of timing-based mutual exclusion with random times. SIAM J. Comput. 31(3), 816–837 (2001)
Bucci, G., Fedeli, A., Luigi Sassoli, L., Vicario, E.: Timed state space analysis of real-time preemptive systems. Trans. Softw. Eng. 30(2), 97–111 (2004)
Cicirelli, F., Nigro, L.: Modelling and verification of mutual exclusion algorithms. In: Proceedings of IEEE/ACM 20th International Symposium on Distributed Simulation and Real Time Application, pp. 136–144 (2016)
Dijkstra, E.W.: Solution of a problem in concurrent programming control. Comm. ACM 8(9), 569 (1965)
Cicirelli, F., Nigro, C., Nigro, L.: Qualitative and quantitative evaluation of stochastic Time Petri nets. In: Proceedings of 2nd International Workshop on Cyber-Physical Systems (IWCPS’15), Lodz, Poland, pp. 775–784 (2015)
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In Proceedings of CAV 2011, pp. 585–591 (2011)
Carullo, L., Furfaro, A., Nigro, L., Pupo, F.: Modelling and simulation of complex systems using TPN Designer. Simul. Model. Pract. Theory 11(7–8), 503–532 (2003)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Nigro, C., Nigro, L., Sciammarella, P.F. (2019). Modelling and Analysis of Partially Stochastic Time Petri Nets Using Uppaal Model Checkers. In: Arai, K., Bhatia, R., Kapoor, S. (eds) Intelligent Computing. CompCom 2019. Advances in Intelligent Systems and Computing, vol 998. Springer, Cham. https://doi.org/10.1007/978-3-030-22868-2_66
Download citation
DOI: https://doi.org/10.1007/978-3-030-22868-2_66
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-22867-5
Online ISBN: 978-3-030-22868-2
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)