Fluid Model-Checking in UPPAAL for Covid-19 | SpringerLink
Skip to main content
Springer Nature Link
Log in

Fluid Model-Checking in UPPAAL for Covid-19

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles (ISoLA 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12476))

Included in the following conference series:

Abstract

During the spring of 2020, the BEOCOVID project has been funded to investigate the use of stochastic hybrid models, statistical model checking and machine learning to analyse, predict and control the rapid spreading of Covid-19 . In this paper we focus on the SEIHR epidemiological model instance of Covid-19 pandemics and show how the risk of viral exposure, the impact of super-spreader events as well as other scenarios can be modelled, estimated and controlled using the tool .

The project was funded by Poul Due Jensens Foundation grant.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 9723
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 12154
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    https://www.ssi.dk.

  2. 2.

    Assuming a fixed number of compartments.

  3. 3.

    Assuming, of course, that the given model is valid with respect to reality.

  4. 4.

    https://www.sst.dk/da/corona/tal-og-overvaagning.

  5. 5.

    https://smittestop.dk/.

  6. 6.

    https://sum.dk/Aktuelt/Nyheder/Coronavirus/2020/Maj/~/media/Filer%20-%20dokumenter/01-corona/App/Politisk-aftale-om-smittessporingsappen.pdf.

  7. 7.

    https://smittestop.dk/spoergsmaal-og-svar.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  Google Scholar 

  2. Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 333–347. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32940-1_24

    Chapter  Google Scholar 

  3. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397–415 (2015)

    Article  Google Scholar 

  4. Jensen, P.G., Jørgensen, K.Y., Larsen, K.G., Mikucionis, M., Muñiz, M., Poulsen, D.B.: Fluid models in uppaal for covid-19 - full models. https://github.com/DEIS-Tools/uppaal-models/tree/master/CaseStudies/Covid-19

  5. Kermack, W.O., McKendrick, A.G.: Contributions to the mathematical theory of epidemics–I. Bull. Math. Biol. 53(1), 33–55 (1991)

    Google Scholar 

  6. Kermack, W.O., McKendrick, A.G.: Contributions to the mathematical theory of epidemics-II. The problem endemicity. Bull. Math. Biol. 53(1), 57–87 (1991)

    Google Scholar 

  7. Kermack, W.O., McKendrick, A.G.: Contributions to the mathematical theory of epidemics-III. Further studies of the problem of endemicity. Bull. Math. Biol. 53(1), 89–118 (1991)

    MATH  Google Scholar 

  8. Peng, L., Yang, W., Zhang, D., Zhuge, C., Hong, L.: Epidemic analysis of covid-19 in China by dynamical modeling (2020)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Aalborg, Denmark

    Peter G. Jensen, Kenneth Y. Jørgensen, Kim G. Larsen, Marius Mikučionis, Marco Muñiz & Danny B. Poulsen

Authors
  1. Peter G. Jensen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kenneth Y. Jørgensen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Marius Mikučionis
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Marco Muñiz
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Danny B. Poulsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Kim G. Larsen or Danny B. Poulsen .

Editor information

Editors and Affiliations

  1. Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Jensen, P.G., Jørgensen, K.Y., Larsen, K.G., Mikučionis, M., Muñiz, M., Poulsen, D.B. (2020). Fluid Model-Checking in UPPAAL for Covid-19. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles. ISoLA 2020. Lecture Notes in Computer Science(), vol 12476. Springer, Cham. https://doi.org/10.1007/978-3-030-61362-4_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-61362-4_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-61361-7

  • Online ISBN: 978-3-030-61362-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics