Verifying AbC Specifications via Emulation

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.