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. © 2013 IFIP International Federation for Information Processing.
CITATION STYLE
Griesmayer, A., & Lomuscio, A. (2013). Model checking distributed systems against temporal-epistemic specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7892 LNCS, pp. 130–145). https://doi.org/10.1007/978-3-642-38592-6_10
Mendeley helps you to discover research relevant for your work.