We propose a methodology for verifying specifications written in AbC, a process calculus for collective systems with a novel communication mechanism relying on predicates over attributes exposed by the components. We emulate the execution of AbC actions and the operators that compose them as programs where guarded sequential functions are non-deterministically invoked; specifically, we translate AbC specifications into sequential C programs. This enables us to use state-of-the-art bounded model checkers for verifying properties of AbC systems. To vindicate our approach, we consider different case studies from different areas and model them as AbC systems, then we translate these AbC specifications into C and instrument the resulting program for verification, finally we perform actual verification of properties of interest.

Verifying AbC Specifications via Emulation

De Nicola, Rocco;Inverso, Omar
2020

Abstract

We propose a methodology for verifying specifications written in AbC, a process calculus for collective systems with a novel communication mechanism relying on predicates over attributes exposed by the components. We emulate the execution of AbC actions and the operators that compose them as programs where guarded sequential functions are non-deterministically invoked; specifically, we translate AbC specifications into sequential C programs. This enables us to use state-of-the-art bounded model checkers for verifying properties of AbC systems. To vindicate our approach, we consider different case studies from different areas and model them as AbC systems, then we translate these AbC specifications into C and instrument the resulting program for verification, finally we perform actual verification of properties of interest.
978-3-030-61469-0
978-3-030-61470-6
Attribute-based communication, Formal analysis, Bounded model checking
File in questo prodotto:
File Dimensione Formato  
2020_ISoLA_ 12477_DeNicola.pdf

non disponibili

Licenza: Non pubblico
396.59 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/20.500.12571/11312
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact