QUANTICOL - A CAS-SCEL implementation for smart-city modelling

This deliverable presents the rst release of the carma Eclipse plug-in, the software tool supporting the carma process algebra and specification language developed in WP4 and discussed in D4.2. We show carma in practice, applied to the analysis of a smart-city model. More specifically, we present an executable carma implementation of a distributed protocol based on coalitional game theory for power trading and coordination in a smart grid, recently proposed in [ST15] and also discussed in D1.3. In this respect, this contribution complements D4.2. While in D4.2 a model of a public transportation system has been specifically developed to showcase the features of carma, here the goal is to demonstrate how carma is expressive enough to describe a realistic smart-grid scenario that has been originally studied independently from the development of the language. The model is presented in a tutorial style, which serves as a guide to the usage of the carma Eclipse plug-in. In addition, the deliverable discusses a number of satellite tools that have been developed during the course of the second reporting period. While the development activities have been mostly decoupled from those of the carma Eclipse plug-in, these tools implement techniques that have the potential to be integrated in future releases to enable further forms of analysis than those currently supported for CAS modelling. Specifically, the Bus Data Visualizer implements real-data visualisation methods as well as techniques for model validation using measurements; FlyFast is a basis for the integration of efficient model-checking techniques; CRNReducer implements model-reduction algorithms; nally, the PALOMA Eclipse plug-in features deterministic approximation techniques based on moment closures. All the reported tools can be reached from http://quanticol.sourceforge.net/.