%0 Conference Proceedings
%T Model Checking Distributed Systems against Temporal-Epistemic Specifications
%+ ARM Ltd [Cambridge] (ARM)
%+ Imperial College London
%A Griesmayer, Andreas
%A Lomuscio, Alessio
%Z Part 5: Session 4: DisCoTec Joint Session
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE)
%C Florence, Italy
%Y Dirk Beyer
%Y Michele Boreale
%I Springer
%3 Formal Techniques for Distributed Systems
%V LNCS-7892
%P 130-145
%8 2013-06-03
%D 2013
%R 10.1007/978-3-642-38592-6_10
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X Concurrency and message reordering are two main causes for the state-explosion in distributed systems with asynchronous communication. We study this domain by analysing ABS, an executable modelling language for object-based distributed systems and present a symbolic model checking methodology for verifying ABS programs against temporal-epistemic specifications. Specifically, we show how to map an ABS program into an ISPL program for verification with MCMAS, a model checker for multi-agent systems. We present a compiler implementing the formal map, exemplify the methodology on a mesh network use case and report experimental results.
%G English
%2 https://inria.hal.science/hal-01515241/document
%2 https://inria.hal.science/hal-01515241/file/978-3-642-38592-6_10_Chapter.pdf
%L hal-01515241
%U https://inria.hal.science/hal-01515241
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-7892