Verifying Temporal Properties of Stigmergic Collective Systems Using CADP

Luca Di Stefano and Frédéric Lang

Proceedings of the 10th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'2021), Rhodes, Greece, October 25-29, 2021

Abstract:

We introduce an automated workflow to verify a variety of temporal properties on systems of agents that interact through virtual stigmergies. By mechanically reducing the property and the system under verification to an MCL query and a sequential LNT program (both MCL and LNT being languages available in the CADP formal verification toolbox), we may reuse efficient model-checking procedures that can give us a verdict on whether the property is satisfied by the system. Among other things, this procedure allows us to verify that a system satisfies a given predicate infinitely often during its execution, which is an improvement over previous verification approaches. We demonstrate the capabilities of this workflow by verifying a selection of example systems. Additionally, we present preliminary results showing that this workflow may also generate parallel LNT programs and exploit compositional verification techniques, which is likely to improve the analysis performance.

16 pages

PDF

PostScript