Statistical Model Checking for Composite Actor Systems

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.
Type de document :
Communication dans un congrès
Narciso Martí-Oliet; Miguel Palomino. 21th InternationalWorkshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. Springer, Lecture Notes in Computer Science, LNCS-7841, pp.143-160, 2013, Recent Trends in Algebraic Development Techniques. 〈10.1007/978-3-642-37635-1_9〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01485983
Contributeur : Hal Ifip <>
Soumis le : jeudi 9 mars 2017 - 15:33:50
Dernière modification le : jeudi 9 mars 2017 - 15:36:07
Document(s) archivé(s) le : samedi 10 juin 2017 - 14:31:16

Fichier

978-3-642-37635-1_9_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Jonas Eckhardt, Tobias Mühlbauer, José Meseguer, Martin Wirsing. Statistical Model Checking for Composite Actor Systems. Narciso Martí-Oliet; Miguel Palomino. 21th InternationalWorkshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. Springer, Lecture Notes in Computer Science, LNCS-7841, pp.143-160, 2013, Recent Trends in Algebraic Development Techniques. 〈10.1007/978-3-642-37635-1_9〉. 〈hal-01485983〉

Partager

Métriques

Consultations de la notice

75

Téléchargements de fichiers

28