Programming and verifying systems relying on attribute-based communications

Collective adaptive systems (CAS) are large conglomerates of interacting components which may be not entirely aware of themselves as members of a group and have limited mutual knowledge and rely only on local rules. However, sophisticated and hardly predictable behaviours often emerges from components interaction. The distinguishing features of CAS, namely adaptivity, anonymity, scalability, open-endedness make them attractive as models of modern systems but challenges practitioners to properly engineer and exploit their power. Attribute based communication is a recently proposed communication paradigm that seems to be particularly appropriate for CAS programming. This novel communication mechanism relies on send and receive primitives that allow selective multicast communication by means of predicates on the attributes exposed in the interface of components among interacting components. Indeed, attribute based communication offers high-level linguistic primitives to deal with CAS, but its practical impact to the actual CAS programming has not been fully investigated yet due to the lacking of efficient run-time environment and programming techniques, and this has prevented practical use. In this thesis, we study the impact and the performances of attribute based communication from the programming and verification point of views. We take as starting point the recently proposed AbC process calculus and proceed by embedding its primitives in Erlang. We follow two different approaches. First, we implement in Erlang the process calculus AbC to come up with ABEL, a domain specific framework with an API very close to that of AbC and with a semantics fully faithful to that of AbC. Then, we introduce AErlang a direct extension of Erlang with attribute-based interaction primitives. We show that, by relying on a verification backend whose input is used as target of a structural translation of AbC systems, properties of ABEL programs can be verified by model checking. We instead evaluate the efficacy of embedding attribute based communication in the actorbased programming model by an extensive evaluation of AErlang on a number of case studies. The evaluation confirms that the overhead resulting from the new communication primitives is acceptable, and that AErlang prototype successfully preserves Erlang efficiency and scalability.