A Framework for Simulation and Symbolic State Space Analysis of Non-Markovian Models

  • Laura Carnevali
  • Lorenzo Ridi
  • Enrico Vicario
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6894)


Formal methods supporting development of safety-critical systems require tools that can be integrated within composed environments. Sirio is a framework for simulation and analysis of various timed extensions of Petri Nets, supporting correctness verification and quantitative evaluation of timed concurrent systems. As a characterizing trait, Sirio is expressly designed to support reuse and to facilitate extensions such as the definition of new reward measures, new variants of the analysis, and new models with a different semantics. We describe here the functional responsibilities and the SW architecture of the framework.


Correctness verification quantitative evaluation preemptive Time Petri Net non-Markovian Stochastic Petri Net stochastic Time Petri Net symbolic state space analysis steady state evaluation transient evaluation 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Lee, I., Sokolsky, O.: Compositional refinement for hierarchical hybrid systems. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 33–48. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Berthomieu, B., Diaz, M.: Modeling and Verification of Time Dependent Systems Using Time Petri Nets. IEEE Trans. on SW Eng. 17(3), 259–273 (1991)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA – Construction of Abstract State Spaces for Petri Nets and Time Petri Nets. International Journal of Production Research 42(14), 2741–2756 (2004)CrossRefzbMATHGoogle Scholar
  4. 4.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL: a Tool-Suite for Automatic Verification of Real-Time Systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  6. 6.
    Bobbio, A., Puliafito, A., Scarpa, M., Telek, M.: WebSPN: A WEB-Accessible Petri Net Tool. In: Proc. Conf. on Web-based Modeling and Simulation (1998)Google Scholar
  7. 7.
    Bondavalli, A., Mura, I., Chiaradonna, S., Filippini, R., Poli, S., Sandrini, F.: DEEM: a tool for the dependability modeling and evaluation of multiple phased systems. In: IEEE Int. Conf. on Dependable Systems and Networks, DSN (June 2000)Google Scholar
  8. 8.
    Bucci, G., Carnevali, L., Ridi, L., Vicario, E.: Oris: a Tool for Modeling, Verification and Evaluation of Real-Time Systems. Int. Journal of Software Tools for Technology Transfer 12(5), 391–403 (2010)CrossRefGoogle Scholar
  9. 9.
    Carnevali, L., Giuntini, J., Vicario, E.: A symbolic approach to quantitative analysis of preemptive real-time systems with non-markovian temporal parameters. In: VALUETOOLS (May 2011)Google Scholar
  10. 10.
    Carnevali, L., Grassi, L., Vicario, E.: State-Density Functions over DBM Domains in the Analysis of Non-Markovian Models. IEEE Trans. on SW Eng. 35(2), 178–194 (2009)CrossRefGoogle Scholar
  11. 11.
    Carnevali, L., Ridi, L., Vicario, E.: Putting preemptive Time Petri Nets to work in a V-model SW life cycle. IEEE Trans. on SW Eng., (accepted for publication)Google Scholar
  12. 12.
    Carnevali, L., Ridi, L., Vicario, E.: Partial stochastic characterization of timed runs over DBM domains. In: Proc. of the 9th International Workshop on Performability Modeling of Computer and Communication Systems (September 2009)Google Scholar
  13. 13.
    CENELEC. EN 50128 - Railway applications: SW for railway control and protection systems (1997)Google Scholar
  14. 14.
    Ciardo, G., German, R., Lindemann, C.: A characterization of the stochastic process underlying a stochastic Petri net. IEEE Trans. On SW Eng. 20(7), 506–515 (1994)CrossRefGoogle Scholar
  15. 15.
    Courtney, T., Gaonkar, S., Keefe, K., Rozier, E., Sanders, W.H.: Möbius 2.3: An extensible tool for dependability, security, and performance evaluation of large and complex system models. In: IEEE/IFIP Int. Conf. on Dependable Systems and Networks (DSN), pp. 353–358 (2009)Google Scholar
  16. 16.
    Vicario, E.: Static Analysis and Dynamic Steering of Time Dependent Systems Using Time Petri Nets. IEEE Trans. on SW Eng. 27(1), 728–748 (2001)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Fersman, E., Krcal, P., Pettersson, P., Yi, W.: Task automata: Schedulability, decidability and undecidability. Inf. Comput. 205(8), 1149–1172 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Timed State Space Analysis of Real Time Preemptive Systems. IEEE Trans. SW Eng. 30(2), 97–111 (2004)CrossRefGoogle Scholar
  19. 19.
    Gardey, G., Lime, D., Magnin, M., Roux, O.: Romeo: A Tool for Analyzing Time Petri Nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  20. 20.
    Gribaudo, M., Codetta-Raiteri, D., Franceschinis, G.: Draw-net, a customizable multi-formalism, multi-solution tool for the quantitative evaluation of systems. In: Int. Conf. on the Quantitative Evaluation of Systems (2005)Google Scholar
  21. 21.
    Henzinger, T.A., Horowitz, B., Kirsch, C.M.: Giotto: A time-triggered language for embedded programming. In: Proc. of the IEEE, pp. 84–99. IEEE, Los Alamitos (2003)Google Scholar
  22. 22.
    Horvath, A., Ridi, L., Vicario, E.: Transient analysis of generalised semi-markov processes using transient stochastic state classes. In: Proc. of the Int. Conf. on Quant. Eval. of Systems, QEST 2010 (2010)Google Scholar
  23. 23.
    Iacono, M., Gribaudo, M.: Element based semantics in multi formalism performance models. In: IEEE Int. Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS), pp. 413–416 (2010)Google Scholar
  24. 24.
    Kulkarni, V.G.: Modeling and analysis of stochastic systems. Chapman & Hall, Ltd., London (1995)zbMATHGoogle Scholar
  25. 25.
    Jordan, P.: IEC 62304 International Standard Edition 1.0 Medical device software - Software life cycle processes. In: The Institution of Engineering and Technology Seminar on Software for Medical Devices 2006 (2006)Google Scholar
  26. 26.
    Merlin, P., Farber, D.J.: Recoverability of Communication Protocols. IEEE Trans. on Comm. 24(9), 1036–1043 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Glynn, P.W.: A GSMP formalism for discrete-event systems. Proceedings of the IEEE 77, 14–23 (1989)CrossRefGoogle Scholar
  28. 28.
    Alur, R., Dill, D.L.: Automata for Modeling Real-Time Systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  29. 29.
    Radio Technical Commission for Aeronautics. DO-178B, Software Considerations in Airborne Systems and Equipment Certification (1992)Google Scholar
  30. 30.
    Sahnerand, R.A., Trivedi, K.S.: Reliability Modeling Using SHARPE. IEEE Trans. on Reliability 36(2), 186–193 (1987)CrossRefGoogle Scholar
  31. 31.
  32. 32.
    Trivedi, K.S., Sahner, R.A.: Sharpe at the age of twenty two. ACM SIGMETRICS Perf. Eval. Review 36(4), 52–57 (2009)CrossRefGoogle Scholar
  33. 33.
    Vicario, E., Sassoli, L., Carnevali, L.: Using Stochastic State Classes in Quantitative Evaluation of Dense-Time Reactive Systems. IEEE Trans. on SW Eng. 35(5), 703–719 (2009)CrossRefGoogle Scholar
  34. 34.
    Vittorini, V., Iacono, M., Mazzocca, N., Franceschinis, G.: The OsMoSys approach to multi-formalism modeling of systems. Software and Systems Modeling 3, 68–81 (2004)CrossRefzbMATHGoogle Scholar
  35. 35.
    Zimmermann, A.: Dependability evaluation of complex systems with timenet. In: Proc. Int. Workshop on Dynamic Aspects in Dependability Models for Fault-Tolerant Systems, DYADEM-FTS 2010 (2010)Google Scholar
  36. 36.
    Zimmermann, A., Freiheit, J., German, R., Hommel, G.: Petri Net Modelling and Performability Evaluation with TimeNET 3.0. In: Haverkort, B.R., Bohnenkamp, H.C., Smith, C.U. (eds.) TOOLS 2000. LNCS, vol. 1786, pp. 188–202. Springer, Heidelberg (2000)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Laura Carnevali
    • 1
  • Lorenzo Ridi
    • 1
  • Enrico Vicario
    • 1
  1. 1.Dipartimento di Sistemi e InformaticaUniversità di FirenzeItaly

Personalised recommendations