Verifying Temporal Properties of Stigmergic Collective Systems Using CADP
Résumé
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 modelchecking 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.
Origine : Fichiers produits par l'(les) auteur(s)