A systematic approach to programming and verifying attribute-based communication systems
De Nicola R., Duong T., Inverso O., Mazzanti F.
Formal modelling Collective-adaptive systems Autonomous systems Formal verification
A methodology is presented for the systematic development of systems of many components, that interact by relying on predicates over attributes that they themselves mutually expose. The starting point is a novel process calculus AbC (for Attribute-based Communication) introduced for modelling collective-adaptive systems. It is shown how to refine the model by introducing a translator from AbC into UML- like state machines that can be analyzed by UMC. In order to execute the specification, another translator is introduced that maps AbC terms into ABEL, a domain-specific framework that offers faithful AbC-style programming constructs built on top of Erlang. It is also shown how the proposed methodology can be used to assess relevant properties of systems and to automatically obtain an executable program for a non- trivial case study.
Source: From Software Engineering to Formal Methods and Tools, and Back. Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday, edited by Maurice H. ter Beek, Alessandro Fantechi, Laura Semini, pp. 377–396. Basel: Springer Nature Switzerland, 2019
Publisher: Springer Nature Switzerland, Basel, CHE
Metrics
Back to previous page
@inbook{oai:it.cnr:prodotti:408346,
title = {A systematic approach to programming and verifying attribute-based communication systems},
author = {De Nicola R. and Duong T. and Inverso O. and Mazzanti F.},
publisher = {Springer Nature Switzerland, Basel, CHE},
doi = {10.1007/978-3-030-30985-5_22},
booktitle = {From Software Engineering to Formal Methods and Tools, and Back. Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday, edited by Maurice H. ter Beek, Alessandro Fantechi, Laura Semini, pp. 377–396. Basel: Springer Nature Switzerland, 2019},
year = {2019}
}
0000-0003-4562-8777