Advertisement

Modelling and Analysis of Partially Stochastic Time Petri Nets Using Uppaal Model Checkers

  • Christian Nigro
  • Libero NigroEmail author
  • Paolo F. Sciammarella
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 998)

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.

Keywords

Time Petri Nets Stochastic behavior Timing constraints Fisher’s mutual exclusion Model checking Statistical model checking Uppaal 

References

  1. 1.
    Jafari, A., Khamespanah, E., Sirjani, M., Hermanns, H.: Performance analysis of distributed and asynchronous systems using probabilistic timed actors. AVoCS 2014, The Netherlands (2014)Google Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Paolieri, M., Horváth, A., Vicario, E.: Probabilistic model checking of regenerative concurrent systems. IEEE Trans. Soft. Eng. 42, 153–169 (2016)CrossRefGoogle Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    Nigro, L., Sciammarella, P.F.: Qualitative and quantitative model checking of distributed probabilistic timed actors. Simul. Model. Pract. Theory 87, 343–368 (2018)CrossRefGoogle Scholar
  6. 6.
    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.004CrossRefGoogle Scholar
  7. 7.
    Merlin, P.M., Farber, D.J.: Recoverability of communication protocols: implications of a theoretical study. IEEE Trans. Commun. 24(9), 1036–1043 (1976)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using Time Petri Nets. IEEE Trans. Soft. Eng. 17(3), 259–273 (1991)MathSciNetCrossRefGoogle Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)MathSciNetCrossRefGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    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
  15. 15.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  16. 16.
    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
  17. 17.
    Gafni, E., Mitzenmaker, M.: Analysis of timing-based mutual exclusion with random times. SIAM J. Comput. 31(3), 816–837 (2001)MathSciNetCrossRefGoogle Scholar
  18. 18.
    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)CrossRefGoogle Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    Dijkstra, E.W.: Solution of a problem in concurrent programming control. Comm. ACM 8(9), 569 (1965)CrossRefGoogle Scholar
  21. 21.
    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)Google Scholar
  22. 22.
    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)CrossRefGoogle Scholar
  23. 23.
    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)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Christian Nigro
    • 1
  • Libero Nigro
    • 1
    Email author
  • Paolo F. Sciammarella
    • 1
  1. 1.DIMESUniversity of CalabriaRendeItaly

Personalised recommendations