Skip to main content
SpringerLink
Log in

Formal Modeling and Analysis of Probabilistic Real-Time Systems

  • Conference paper
  • First Online:
Fourth International Congress on Information and Communication Technology

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 1041))

  • 696 Accesses

Abstract

This paper considers formal modeling and analysis of distributed timed and stochastic real-time systems. The approach is based on Stochastic Time Petri Nets (sTPN) which offer a readable yet powerful modeling language. sTPN are supported by special case tools which can ensure accuracy in the results by numerical methods and the enumeration of stochastic state classes. These techniques, though, can suffer of state explosion problems when facing large models. In this work, a reduction of sTPN onto the popular Uppaal model checkers is developed which permits both exhaustive non-deterministic analysis, which ignores stochastic aspects and it is useful for functional and temporal assessment of system behavior, and quantitative analysis through statistical model checking, useful for estimating by automated simulation runs probability measures of event occurrence. The paper provides the formal definition of sTPN and its embedding into Uppaal. A sensor network case study is used as a running example throughout the paper to demonstrate the practical applicability of the approach.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. A. Jafari, E. Khamespanah, M. Sirjani, H. Hermanns, M. Cimini, PTRebeca: modeling and analysis of distributed and asynchronous systems. Sci. Comput. Program. 128, 22–50 (2016)

    Article  Google Scholar 

  2. L. Nigro, P.F. Sciammarella, Qualitative and quantitative model checking of distributed probabilistic timed actors. Simul. Model. Pract. Theory 87, 343–368 (2018)

    Article  Google Scholar 

  3. E. Vicario, L. Sassoli, L. Carnevali, Using stochastic state classes in quantitative evaluation of dense-time reactive systems. IEEE Trans. on Soft. Eng. 35(5), 703–719 (2009)

    Article  Google Scholar 

  4. L. Carnevali, L. Grassi, E. Vicario, State-density functions over DBM domains in the analysis of non-Markovian models. IEEE Trans. on SW Eng. 35(2):178–194 (2009)

    Google Scholar 

  5. F. Cicirelli, C. Nigro, L. Nigro, Qualitative and quantitative evaluation of stochastic Time Petri Nets, in 2015 Federated Conference on Computer Science and Information Systems (FedCSIS), (IEEE, 2015), pp. 763–772

    Google Scholar 

  6. 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 12, 391–403 (2010)

    Google Scholar 

  7. Uppaal, on-line: www.uppaal.org

  8. G. Behrmann, A. David, K.G. Larsen, A tutorial on Uppaal, in Formal Methods for the Design of Real-Time Systems, vol. 3185, ed. by M. Bernardo, F. Corradini Lecture Notes in Computer Science (Springer-Verlag, 2004), pp. 200–236

    Google Scholar 

  9. A. David, K.G. Larsen, A. Legay, M. Mikucionis, D.B. Poulsen, Uppaal SMC tutorial. Int. J. on Software Tools for Technology Transfer 17, 1–19 (2015). https://doi.org/10.1007/s10009-014-0361-y

  10. 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

  11. T. Murata, Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541–580 (1989)

    Article  Google Scholar 

  12. P.M. Merlin, D.J. Farber, Recoverability of communication protocols: implications of a theoretical study. IEEE Trans. Commun. 24(9), 1036–1043 (1976)

    Article  MathSciNet  Google Scholar 

  13. B. Berthomieu, M. Diaz, Modeling and verification of time dependent systems using Time Petri Nets. IEEE Trans. Soft. Eng. 17(3), 259–273 (1991)

    Article  MathSciNet  Google Scholar 

  14. E.A. Lee, M. Sirjani, What good are models? in International Conference on Formal Aspects of Component Software, (Springer, Cham, 2018), pp. 3–31

    Google Scholar 

  15. L. Carullo, A. Furfaro, L. Nigro, F. Pupo, Modelling and simulation of complex systems using TPN designer. Simul. Model. Pract. Theory 11(7-8), 503–532 (2003)

    Article  Google Scholar 

  16. C. Nigro, L. Nigro, P.F. Sciammarella, Modelling and analysis of multi-agent systems using UPPAAL SMC. Int. J. Simul. Process Model. 13(1), 73–87 (2018)

    Article  Google Scholar 

  17. G.D. Plotkin, A structural approach to operational semantics (1981)

    Google Scholar 

  18. M.A. Marsan, G. Balbo, G. Conte, S. Donatelli, G. Franceschinis, Modelling with generalized stochastic Petri nets (Wiley, 2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Independent Computer Professional, Rende, Italy

    Christian Nigro

  2. DIMES, University of Calabria, Rende, Italy

    Libero Nigro & Paolo F. Sciammarella

Authors
  1. Christian Nigro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Libero Nigro
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paolo F. Sciammarella
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Libero Nigro .

Editor information

Editors and Affiliations

  1. School of Science and Technology, Middlesex University, London, UK

    Xin-She Yang

  2. University of Reading, Reading, UK

    Simon Sherratt

  3. Department of Information Technology, Techno India College of Technology, Kolkata, West Bengal, India

    Nilanjan Dey

  4. Global Knowledge Research Foundation, Ahmedabad, Gujarat, India

    Amit Joshi

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Singapore Pte Ltd.

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Nigro, C., Nigro, L., Sciammarella, P.F. (2020). Formal Modeling and Analysis of Probabilistic Real-Time Systems. In: Yang, XS., Sherratt, S., Dey, N., Joshi, A. (eds) Fourth International Congress on Information and Communication Technology. Advances in Intelligent Systems and Computing, vol 1041. Springer, Singapore. https://doi.org/10.1007/978-981-15-0637-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-981-15-0637-6_5

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-15-0636-9

  • Online ISBN: 978-981-15-0637-6

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation