SLiVER Tool for Modeling and Analyzing Multi-agent Systems

Organisation:	Gran Sasso Science Institute, L'Aquila and IMT School of Advanced Studies, Lucca (ITALY) CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
Functionality:	Multi-agent Systems
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2019-2020
Description:	Multi-agent systems (MAS) are composed of standalone computational units (the agents) interacting with each other and with an external environment. Computation within each agent may be a composition of multiple interleaving processes, and agents may also (possibly asynchronously) interact with each other. As a result, MAS typically feature extremely large state spaces, which makes them hard to design and reason about. Therefore, there is a need for languages allowing to specify these systems in a concise and intuitive fashion, as well as tools that can certify or increase confidence in the correctness of MAS specifications. However, the development of tools for such new languages may be a daunting task, as it must keep pace with both the evolution of the language and the state of the art in formal analysis of systems. An alternative solution is to encode a MAS specification into an existing language, and reuse mature tools for that language to analyze the encoded system. This is the approach adopted in SLiVER, a prototype tool for the automated verification of MAS described in the simple specification language LAbS. SLiVER is highly modular: it exploits the formal semantics of LAbS to encode the input system into an emulation program in a given language, through a structural translation procedure, and verifies the emulation program with off-the-shelf tools for that language to reach a verdict on the correctness of the input system. SLiVER can generate two types of outputs: sequential C programs, which are verified using bounded model checking tools such as 2LS, CBMC, and ESBMC; and LNT programs, which are verified using CADP. The LNT workflow is implemented as a SLiVER module and can verify both invariance properties (i.e., all reachable states satisfy a given MCL formula) and inevitable reachability ones (i.e., all executions lead to a state where the given MCL formula is satisfied), over the full state space of the input system. The LNT workflow also enables to simulate the evolution of the system and produce a set of execution traces. This provides a valuable design aid and can give a quick feedback even on very large systems.
Conclusions:	The need to analyze MAS to establish their correctness is felt far beyond the multi-agent community, as agent-based models are gaining popularity in economics, social sciences, biology, and many other research fields. The SLiVER tool provides an automated analysis workflow for MAS based on LNT and CADP. The workflow allows to formally verify the input system via model checking, as well as to generate simulation traces. The end user does not need to be familiar with either LNT or CADP: knowledge of the input language LAbS is the only requirement.
Publications:	[DiStefano-20] Luca Di Stefano. "Modelling and Verification of Multi-Agent Systems via Sequential Emulation". PhD thesis, Gran Sasso Science Institute, L'Aquila, October 2020. Available on-line at: https://www.researchgate.net/publication/344672355_Modelling_and_Verification_of_Multi-Agent_Systems_via_Sequential_Emulation or from the CADP Web site in PDF or PostScript [DiStefano-Lang-Serwe-20] Luca Di Stefano, Frédéric Lang, and Wendelin Serwe. "Combining SLiVER with CADP to Analyze Multi-agent Systems". Proceedings of the 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION'2020), La Valetta, Malta, Lecture Notes in Computer Science vol. 12134, pp. 370-385. Springer Verlag, June 2020. Available on-line at: https://hal.inria.fr/hal-02890401/en or from the CADP Web site in PDF or PostScript [DiStefano-Lang-21] Luca Di Stefano and Frédéric Lang. "Verifying Temporal Properties of Stigmergic Collective Systems Using CADP". Proc. of the 10th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'2021), Rhodes, Greece, Lecture Notes in Computer Science vol. 13036, pp. 473-489. Springer Verlag, October 2021. Available on-line at: https://hal.inria.fr/hal-03385131/en or from the CADP Web site in PDF or PostScript [DiStefano-Lang-23-a] Luca Di Stefano and Frédéric Lang. "Compositional Verification of Stigmergic Collective Systems". Proc. of the 24th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'2023), Boston, USA, Lecture Notes in Computer Science vol. 13881, pp. 155-176. Springer Verlag, January 2023. Available on-line at: https://hal.inria.fr/hal-03869922/en or from the CADP Web site in PDF or PostScript [DiStefano-Lang-23-b] Luca Di Stefano and Frédéric Lang. "Compositional Verification of Priority Systems using Sharp Bisimulation". Formal Methods in Systems Design, 2023. Available on-line at: https://hal.inria.fr/hal-04103681/en or from the CADP Web site in PDF or PostScript
Contact:	Luca Di Stefano Gran Sasso Science Institute (GSSI) viale Francesco Crispi, 7 67100 L'Aquila ITALY Email: luca.distefano@gssi.it
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page