%0 Conference Proceedings
%T Combining SLiVER with CADP to Analyze Multi-agent Systems
%+ Gran Sasso Science Institute (GSSI)
%+ Construction of verified concurrent systems (CONVECS )
%A Di Stefano, Luca
%A Lang, Frédéric
%A Serwe, Wendelin
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B COORDINATION 2020 - 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages
%C La Valetta, Malta
%I Springer Verlag
%V 12134
%P 370-385
%8 2020-06-15
%D 2020
%R 10.1007/978-3-030-50029-0_23
%Z Computer Science [cs]/Multiagent Systems [cs.MA]
%Z Computer Science [cs]/Software Engineering [cs.SE]Conference papers
%X We present an automated workflow for the analysis of multi-agent systems described in a simple specification language. The procedure is based on a structural encoding of the input system and the property of interest into an LNT program, and relies on the CADP software toolbox to either verify the given property or simulate the encoded system. Counterexamples to properties under verification, as well as simulation traces, are translated into a syntax similar to that of the input language: therefore, no knowledge of CADP is required. The workflow is implemented as a module of the verification tool SLiVER. We present the input specification language, describe the analysis workflow, and show how to invoke SLiVER to verify or simulate two example systems. Then, we provide details on the LNT encoding and the verification procedure.
%G English
%2 https://inria.hal.science/hal-02890401/document
%2 https://inria.hal.science/hal-02890401/file/coordination2020.pdf
%L hal-02890401
%U https://inria.hal.science/hal-02890401
%~ UGA
%~ CNRS
%~ INRIA
%~ INPG
%~ INRIA-RHA
%~ LIG
%~ INRIA_TEST
%~ LIG_MFML_CONVECS
%~ CONVECS
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-COORDINATION
%~ INRIA-RENGRE
%~ UGA-EPE
%~ IFIP-LNCS-12134
%~ LIG_SIDCH