Formal Specification and Validation of a Data-driven Software System for Fire Risk Prediction

Abstract

Long periods of dry and cold weather conditions significantly increase fire risks for wooden buildings. Recent advances in predictive fire risk models combined with publicly available cloud-based weather data services have enabled the development of smart software systems for location-oriented fire risk notification. We have developed a Coloured Petri Net (CPN) model specifying the software architecture of a microservice-based predictive fire risk notification system. The CPN model captures the set of micro-services provided via REST APIs and the interaction between the constituent services for location tracking and subscription, fire risk computation, and data harvesting. As part of the work, we present a general modelling approach and pattern for REST-based APIs. We apply simulation and state space exploration to validate and verify key behavioural properties of the predictive fire risk notification system.