Modeling and Efficient Verification of Broadcasting Actors

Abstract : Many distributed systems use broadcast communication for various reasons such as saving energy or increasing throughput. However, the actor model for concurrent and distributed systems does not directly support this kind of communication. In such cases, a broadcast must be modeled as multiple unicasts which leads to loss of modularity and state space explosion for any non-trivial system. In this paper, we extend Rebeca, an actor-based model language, to support asynchronous anonymous message broadcasting. Then, we apply counter abstraction for reducing the state space which efficiently bypasses the constructive orbit problem by considering the global state as a vector of counters, one per each local state. This makes the model checking of systems possible without further considerations of symmetry. This approach is efficient for fully symmetric system like broadcasting environments. We use a couple of case studies to illustrate the applicability of our method and the way their state spaces are reduced in size.
Type de document :
Communication dans un congrès
Mehdi Dastani; Marjan Sirjani. 6th Fundamentals of Software Engineering (FSEN), Apr 2015, Tehran, Iran. Springer, Lecture Notes in Computer Science, LNCS-9392, pp.69-83, 2015, Fundamentals of Software Engineering. 〈10.1007/978-3-319-24644-4_5〉
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01446611
Contributeur : Hal Ifip <>
Soumis le : jeudi 26 janvier 2017 - 10:43:54
Dernière modification le : jeudi 26 janvier 2017 - 10:57:18
Document(s) archivé(s) le : vendredi 28 avril 2017 - 05:40:17

Fichier

978-3-319-24644-4_5_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Behnaz Yousefi, Fatemeh Ghassemi, Ramtin Khosravi. Modeling and Efficient Verification of Broadcasting Actors. Mehdi Dastani; Marjan Sirjani. 6th Fundamentals of Software Engineering (FSEN), Apr 2015, Tehran, Iran. Springer, Lecture Notes in Computer Science, LNCS-9392, pp.69-83, 2015, Fundamentals of Software Engineering. 〈10.1007/978-3-319-24644-4_5〉. 〈hal-01446611〉

Partager

Métriques

Consultations de la notice

37