QUANTICOL - The QUANTICOL software tool suite for modelling smart cities

This deliverable is an account of the QUANTICOL software tool suite, with application to the smart city scenarios studied in the project. While Deliverable D4.3 focuses on the CARMA language and its implementation with the CARMA Eclipse plug-in, in this deliverable we present software tools developed to support further techniques such as model checking, model order reduction, and reachability analysis. Their integration with the CARMA Eclipse plug-in is discussed in Deliverable D4.3. Instead, here we provide detailed account of such tools as stand-alone products. We present FlyFast, a probabilistic model checker for mean-field models; jSSTL, for the analysis of Signal Spatio-Temporal Logic; ERODE, for the reduction of systems of ordinary differential equations; UTOPIC, for the reachability analysis of nonlinear dynamical systems; and topochecker, a spatio-temporal model checker. While an application of FlyFast to smart cities is presented in D4.3, in this deliverable we discuss an application of jSSTL and ERODE to the verification and reduction, respectively, of a model of a bike-sharing system. Instead, bus transportation systems are studied with topochecker, to detect problems in vehicle location data and clumping in frequent services.