Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
State Distribution Policy for Distributed Model Checking of Actor Models
University of Tehran, School of Electrical and Computer Engineering, Tehran, Iran & Reykjavik University, School of Computer Science, Reykjavik, Island.
Reykjavik University, School of Computer Science, Reykjavik, Island.
Halmstad University, School of Information Technology, Halmstad Embedded and Intelligent Systems Research (EIS), Centre for Research on Embedded Systems (CERES).ORCID iD: 0000-0002-4869-6794
University of Tehran, School of Electrical and Computer Engineering, Tehran, Iran.
Show others and affiliations
2015 (English)In: Electronic Communications of the EASST, ISSN 1863-2122, E-ISSN 1863-2122, Vol. 72, 1-15 p.Article in journal (Refereed) Published
Abstract [en]

Model checking temporal properties is often reduced to finding accepting cycles in Buchi automata. A key ingredient for an effective distributed model ¨ checking technique is a distribution policy that does not split the potential accepting cycles of the corresponding automaton among several nodes. In this paper, we introduce a distribution policy to reduce the number of split cycles. This policy is based on the call dependency graph, obtained from the message passing skeleton of the model. We prove theoretical results about the correspondence between the cycles of call dependency graph and the cycles of the concrete state space and provide empirical data obtained from applying our distribution policy in state space generation and reachability analysis. We take Rebeca, an imperative interpretation of actors, as our modeling language and implement the introduced policy in its distributed state space generator. Our technique can be applied to other message-driven actor-based models where concurrent objects or services are units of concurrency.

Place, publisher, year, edition, pages
Berlin: Universitätsverlag der TU Berlin, 2015. Vol. 72, 1-15 p.
Keyword [en]
Distributed Model Checking, State Distribution Policy, Concurrent Ob-jects, Actors, Rebeca
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:hh:diva-29997OAI: oai:DiVA.org:hh-29997DiVA: diva2:878762
Conference
15th International Workshop onAutomated Verification of Critical Systems (AVoCS 2015)
Projects
EFFEMBAC (Vetenskapsrådet, award number 621-2014-5057)AUTO-CAAS (KK Stiftelse)
Funder
Swedish Research Council, 621-2014-5057
Note

The work of M.R. Mousavi has been partially supported by the Swedish Research Council (Vetenskapsra ̊det) with award number 621-2014-5057 (Effective Model-Based Testing of Paral- lel Systems) and the Swedish Knowledge Foundation (Stiftelsen fo ̈r Kunskaps- och Kompeten- sutveckling) in the context of the AUTO-CAAS project.

Available from: 2015-12-09 Created: 2015-12-09 Last updated: 2017-12-01Bibliographically approved

Open Access in DiVA

fulltext(1063 kB)112 downloads
File information
File name FULLTEXT01.pdfFile size 1063 kBChecksum SHA-512
8826dd1e5d6ff70cf85954810db9aaa6eabeba25ff1fda73651c2d5975dfbcb1baaccef21ff5a54aa261d459742d92091eb49ba6d5eae707e1820b3b8ad238bb
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Mousavi, Mohammad Reza
By organisation
Centre for Research on Embedded Systems (CERES)
In the same journal
Electronic Communications of the EASST
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 112 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 113 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf