nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Combining SLiVER with CADP to Analyze Multi-agent Systems

verfasst von : Luca Di Stefano, Frédéric Lang, Wendelin Serwe

Erschienen in: Coordination Models and Languages

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel On Implementing Symbolic Controllability

Nächstes Kapitel Formal Modeling and Analysis of Medical Systems

A Linux release of SLiVER is available at https://git.io/sliver-tool.

CADP is available at http://cadp.inria.fr.

See http://cadp.inria.fr/man/evaluator.html and http://cadp.inria.fr/man/mcl.html.

See http://cadp.inria.fr/man/executor.html.

The full command used to obtain this trace is sliver.py leader.labs n=3 --backend cadp --simulate 1 --steps 100.

The full LNT programs for the dining philosophers system (with \(\texttt {\_n} = 5\)) and the leader election one (with \(\texttt {\_n} = 3\)) can be found at https://git.io/philosophers-lnt and https://git.io/leader-lnt, respectively.

Abd Alrahman, Y., De Nicola, R., Loreti, M.: A calculus for collective-adaptive systems and its behavioural theory. Inf. Comput. 268 (2019). https://doi.org/10.1016/j.ic.2019.104457

Aspnes, J., Ruppert, E.: An introduction to population protocols. In: Garbinato, B., Miranda, H., Rodrigues, L. (eds.) Middleware for Network Eccentric and Mobile Applications, pp. 97–120. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-540-89707-1_5

Axtell, R.L., et al.: Population growth and collapse in a multiagent model of the Kayenta Anasazi in Long House Valley. Proc. Natl. Acad. Sci. 99(suppl 3), 7275–7279 (2002). https://doi.org/10.1073/pnas.092080799MathSciNetCrossRef

Baeza, A., Janssen, M.A.: Modeling the decline of labor-sharing in the semi-desert region of Chile. Reg. Environ. Change 18(4), 1161–1172 (2017). https://doi.org/10.1007/s10113-017-1243-0CrossRef

Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14

Blondin, M., Esparza, J., Jaax, S.: Peregrine: a tool for the analysis of population protocols. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 604–611. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_34CrossRef

Bordini, R.H., Dennis, L.A., Farwer, B., Fisher, M.: Automated verification of multi-agent programs. In: 23rd International Conference on Automated Software Engineering (ASE), pp. 69–78. IEEE (2008). https://doi.org/10.1109/ASE.2008.17

Chen, H.Y., David, C., Kroening, D., Schrammel, P., Wachter, B.: Synthesising interprocedural bit-precise termination proofs. In: 30th International Conference on Automated Software Engineering (ASE), pp. 53–64. IEEE (2015). https://doi.org/10.1109/ASE.2015.10

Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_15CrossRefMATH

10.

De Nicola, R., Di Stefano, L., Inverso, O.: Multi-agent systems with virtual stigmergy. Sci. Comput. Program. 187 (2020). https://doi.org/10.1016/j.scico.2019.102345

11.

De Nicola, R., Duong, T., Inverso, O., Mazzanti, F.: Verifying properties of systems relying on attribute-based communication. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 169–190. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68270-9_9CrossRef

12.

De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-53479-2_17CrossRef

13.

Farmer, J.D., Foley, D.: The economy needs agent-based modelling. Nature 460(7256), 685–686 (2009). https://doi.org/10.1038/460685aCrossRef

14.

Gadelha, M.Y.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an industrial-strength C model checker. In: 33rd International Conference on Automated Software Engineering (ASE), pp. 888–891. ACM (2018). https://doi.org/10.1145/3238147.3240481

15.

Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Informatica 52(4–5), 337–392 (2015). https://doi.org/10.1007/s00236-015-0226-1

16.

Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Softw. Tools Technol. Transf. 15(2), 89–107 (2013). https://doi.org/10.1007/s10009-012-0244-zCrossRefMATH

17.

Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 3–26. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68270-9_1CrossRef

18.

Garavel, H., Salaün, G., Serwe, W.: On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP. Sci. Comput. Program. 74(3), 100–127 (2009). https://doi.org/10.1016/j.scico.2008.09.011MathSciNetCrossRefMATH

19.

Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)

20.

ISO/IEC: LOTOS – A formal description technique based on the temporal ordering of observational behaviour. International Standard 8807 (1989)

21.

Kozen, D.: Results on the propositional \(\upmu \)-Calculus. Theoret. Comput. Sci. 27, 333–354 (1983). https://doi.org/10.1016/0304-3975(82)90125-6MathSciNetCrossRefMATH

22.

Lang, F., Mateescu, R., Mazzanti, F.: Compositional verification of concurrent systems by combining bisimulations. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 196–213. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_13CrossRef

23.

Lang, F., Mateescu, R., Mazzanti, F.: Sharp congruences adequate with temporal logics combining weak and strong modalities. TACAS 2020. LNCS, vol. 12079, pp. 57–76. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45237-7_4CrossRef

24.

Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19(1), 9–30 (2015). https://doi.org/10.1007/s10009-015-0378-xCrossRef

25.

Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_12CrossRef

26.

Pinciroli, C., Lee-Brown, A., Beltrame, G.: A tuple space for data sharing in robot swarms. In: 9th International Conference on Bio-inspired Information and Communications Technologies (BICT), pp. 287–294. ICST/ACM (2015). https://doi.org/10.4108/eai.3-12-2015.2262503

27.

Queille, J.P., Sifakis, J.: Fairness and related properties in transition systems - a temporal logic to deal with fairness. Acta Informatica 19, 195–220 (1983). https://doi.org/10.1007/BF00265555MathSciNetCrossRefMATH

28.

Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_16CrossRef

29.

Stiglitz, J.E., Gallegati, M.: Heterogeneous interacting agent models for understanding monetary economies. Eastern Econ. J. 37(1), 6–12 (2011). https://doi.org/10.1057/eej.2010.33CrossRef

30.

ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119–135 (2011). https://doi.org/10.1016/j.scico.2010.07.002CrossRefMATH

31.

Winikoff, M.: Assurance of agent systems: what role should formal verification play? In: Dastani, M., Hindriks, K., Meyer, J.J. (eds.) Specification and Verification of Multi-Agent Systems, pp. 353–383. Springer, Heidelberg (2010). https://doi.org/10.1007/978-1-4419-6984-2_12

Titel: Combining SLiVER with CADP to Analyze Multi-agent Systems
verfasst von: Luca Di Stefano
Frédéric Lang
Wendelin Serwe
Verlag: Springer International Publishing
Buch: Coordination Models and Languages
Print ISBN: 978-3-030-50028-3

Electronic ISBN: 978-3-030-50029-0

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-50029-0_23

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner