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

Peter Fogh; Thomas Cano Hald; Brian Nielsen

doi:10.1109/CPSData.2016.7496421

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

Peter Fogh, Thomas Cano Hald, Brian Nielsen

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-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 language	English
Title of host publication	2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS (CPS Data)
Number of pages	6
Publisher	IEEE (Institute of Electrical and Electronics Engineers)
Publication date	11 Apr 2016
Pages	1-6
ISBN (Electronic)	978-1-5090-1154-4
DOIs	https://doi.org/10.1109/CPSData.2016.7496421
Publication status	Published - 11 Apr 2016
Event	2nd International Workshop on Modelling, Analysis, and Control of Complex CPS - Wien, Austria Duration: 11 Apr 2016 → … Conference number: 2

Conference

Conference	2nd International Workshop on Modelling, Analysis, and Control of Complex CPS
Number	2
Country/Territory	Austria
City	Wien
Period	11/04/2016 → …

Keywords

Automata
Computational modeling
Web services
Servers
Computer architecture
Memory
Model checking

Access to Document

10.1109/CPSData.2016.7496421

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@inproceedings{142b1eac04cf4f3ab2eb9cd6fd98c063,

title = "WUppaal:: A web-service for the Uppaal model-checker",

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.",

keywords = "Automata, Computational modeling, Web services, Servers, Computer architecture, Memory, Model checking",

author = "Peter Fogh and {Cano Hald}, Thomas and Brian Nielsen",

year = "2016",

month = apr,

day = "11",

doi = "10.1109/CPSData.2016.7496421",

language = "English",

pages = "1--6",

booktitle = "2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS (CPS Data)",

publisher = "IEEE (Institute of Electrical and Electronics Engineers)",

address = "United States",

note = "2nd International Workshop on Modelling, Analysis, and Control of Complex CPS, CPS Data ; Conference date: 11-04-2016",

}

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). IEEE (Institute of Electrical and Electronics Engineers), pp. 1-6, 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS, Wien, Austria, 11/04/2016. https://doi.org/10.1109/CPSData.2016.7496421

WUppaal: A web-service for the Uppaal model-checker. / Fogh, Peter; Cano Hald, Thomas; Nielsen, Brian.
2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS (CPS Data). IEEE (Institute of Electrical and Electronics Engineers), 2016. p. 1-6.

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

T1 - WUppaal:

T2 - 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS

AU - Fogh, Peter

AU - Cano Hald, Thomas

AU - Nielsen, Brian

N1 - Conference code: 2

PY - 2016/4/11

Y1 - 2016/4/11

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

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

KW - Automata

KW - Computational modeling

KW - Web services

KW - Servers

KW - Computer architecture

KW - Memory

KW - Model checking

U2 - 10.1109/CPSData.2016.7496421

DO - 10.1109/CPSData.2016.7496421

M3 - Article in proceeding

SP - 1

EP - 6

BT - 2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS (CPS Data)

PB - IEEE (Institute of Electrical and Electronics Engineers)

Y2 - 11 April 2016

ER -