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.
['Peter Fogh', 'Thomas Cano Hald', 'Brian Nielsen']
WUppaal: A web-service for the Uppaal model-checker