QUANTICOL - CAS-SCEL semantics and implementation

Ciancia V., De Nicola R., Hillston J., Latella D., Loreti M., Massink M.

Stochastic Process Algebras  F.3.1 LOGICS AND MEANINGS OF PROGRAMS . Specifying and Verifying and Reasoning about Programs 

At the end of the first year of the QUANTICOL project, we identified the linguistic primitives and the interaction patterns (such as broadcast communication or anonymous interaction) that are needed to model the QUANTICOL case studies and, more generally, in Collective Adaptive Systems (CAS) design. Starting from these primitives and interaction patterns, in the second reporting period, we have worked on the definition of syntax and semantics of the CAS-SCEL language that we named CARMA (Collective Adaptive Resource-sharing Markovian Agents). CARMA is a language specifically developed for the specification and analysis of CAS, with the specific objective to support quantitive evaluation and verification. CARMA combines the lessons learnt from other stochastic process algebras such as PEPA [21], EMPA [2], MTIPP [20] and MoDEST [3], with those learnt from languages specifically designed to model CAS, such as SCEL [13], the AbC calculus [1], PALOMA [14], and the Attributed Pi calculus [22], which feature attribute-based communication and explicit representation of locations. To support simulation of CARMA models a prototype simulator has been also developed. This simulator, which has been implemented in Java, can be used to perform stochastic simulation and can be used as the basis for implementing other analysis techniques. An Eclipse plug-in for supporting specification and analysis of CAS in CARMA has also been developed. Thanks to this plug-in, CARMA systems can be specified by means of an appropriate high-level language. The high level specification is mapped to a process algebra to enable qualitative and quantitive analysis of CAS during system development by following specific design workflows and analysis pathways. In this deliverable we will describe the so-called CARMA Specification Language while in D5.2 an overview of the CARMA Eclipse Plug-in, together with an example of use, is provided. In this document, we first introduce the syntax of CARMA and its operational semantics; then we describe the CARMA tools and show how the formalism can be used to support the quantitative analysis of a simple scenario. Then, we provide a brief illustration of how CARMA could be extended in order to provide a flexible and structured mechanism for defining common spatial aspects of CAS. The document ends with a description of the direction of future work and the relationship with the work done in the other workpackages of the project.

Source: Project report, QUANTICOL, Deliverable D4.2, 2015