Statistical Model Checking for Composite Actor SystemsReport as inadecuate

Statistical Model Checking for Composite Actor Systems - Download this document for free, or read online. Document in PDF available to download.

1 TUM - Technische Universität München München 2 University of Illinois at Urbana-Champaign Urbana 3 Ludwig-Maximilians-Universität München

Abstract : In this paper we propose the so-called composite actor model for specifying composed entities such as the Internet. This model extends the actor model of concurrent computation so that it follows the -Reflective Russian Dolls- pattern and supports an arbitrary hierarchical composition of entities. To enable statistical model checking we introduce a new scheduling approach for composite actor models which guarantees the absence of unquantified nondeterminism. The underlying executable specification formalism we use is the rewriting logic-based semantic framework Maude, its probabilistic extension PMaude, and the statistical model checker PVeStA. We formalize a model transformation which—given certain formal requirements—generates a scheduled specification. We prove the correctness of the scheduling approach and the soundness of the transformation by introducing the notions of strong zero-time rule confluence and time-passing bisimulation and by showing that the transformation is a time-passing bisimulation for strongly zero-time rule confluent composite actor specifications.

Keywords : actor system rewriting logic Maude composite actor statistical model checking

Author: Jonas Eckhardt - Tobias Mühlbauer - José Meseguer - Martin Wirsing -



Related documents