WUppaal: A web-service for the Uppaal model-checker

Peter Fogh, Thomas Cano Hald, Brian Nielsen

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

1 Citation (Scopus)

Abstract

Model checking tools for complex cyber-physical systems are increasingly being invoked online and incrementally in machine-to-machine scenarios, and executed on remote large scale compute resources. To support these scenarios in a uniform and standardized way, we present the web service WUppaal that provides formal verification of timed automata using the Uppaal model-checker. WUppaal provides easy access to a large amount of resources through a RESTful API. Through a machine-to-machine use case on a job shop scheduling application, we show the practical use of WUPPAAL. Our benchmark shows that the web service can handle the expected load, but a stress test shows that the service can handle more than expected in case of peak hour.
Original languageEnglish
Title of host publication2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS (CPS Data)
Number of pages6
PublisherIEEE
Publication date11 Apr 2016
Pages1-6
ISBN (Electronic)978-1-5090-1154-4
DOIs
Publication statusPublished - 11 Apr 2016
Event2nd International Workshop on Modelling, Analysis, and Control of Complex CPS - Wien, Austria
Duration: 11 Apr 2016 → …
Conference number: 2

Conference

Conference2nd International Workshop on Modelling, Analysis, and Control of Complex CPS
Number2
CountryAustria
CityWien
Period11/04/2016 → …

    Fingerprint

Keywords

  • Automata
  • Computational modeling
  • Web services
  • Servers
  • Computer architecture
  • Memory
  • Model checking

Cite this

Fogh, P., Cano Hald, T., & Nielsen, B. (2016). WUppaal: A web-service for the Uppaal model-checker. In 2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS (CPS Data) (pp. 1-6). IEEE. https://doi.org/10.1109/CPSData.2016.7496421