Skip to Main content Skip to Navigation
New interface
Conference papers

Model Checking Distributed Systems against Temporal-Epistemic Specifications

Abstract : 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.
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, April 27, 2017 - 10:46:46 AM
Last modification on : Tuesday, January 18, 2022 - 2:26:05 PM
Long-term archiving on: : Friday, July 28, 2017 - 12:45:20 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Andreas Griesmayer, Alessio Lomuscio. Model Checking Distributed Systems against Temporal-Epistemic Specifications. 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), Jun 2013, Florence, Italy. pp.130-145, ⟨10.1007/978-3-642-38592-6_10⟩. ⟨hal-01515241⟩



Record views


Files downloads