hh.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • 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.
Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).ORCID-id: 0000-0002-4869-6794
University of Tehran, School of Electrical and Computer Engineering, Tehran, Iran.
Visa övriga samt affilieringar
2015 (Engelska)Ingår i: Electronic Communications of the EASST, ISSN 1863-2122, E-ISSN 1863-2122, Vol. 72, s. 1-15Artikel i tidskrift (Refereegranskat) Published
Abstract [en]

Model checking temporal properties is often reduced to finding accepting cycles in Büchi 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.

Ort, förlag, år, upplaga, sidor
Berlin: Universitätsverlag der TU Berlin, 2015. Vol. 72, s. 1-15
Nyckelord [en]
Distributed Model Checking, State Distribution Policy, Concurrent Ob-jects, Actors, Rebeca
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:hh:diva-29997DOI: 10.14279/tuj.eceasst.72.1022.1011Scopus ID: 2-s2.0-85032947273OAI: oai:DiVA.org:hh-29997DiVA, id: diva2:878762
Konferens
15th International Workshop onAutomated Verification of Critical Systems (AVoCS 2015)
Projekt
EFFEMBAC (Vetenskapsrådet, award number 621-2014-5057)AUTO-CAAS (KK Stiftelse)
Forskningsfinansiär
Vetenskapsrådet, 621-2014-5057
Anmärkning

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.

Tillgänglig från: 2015-12-09 Skapad: 2015-12-09 Senast uppdaterad: 2020-03-23Bibliografiskt granskad

Open Access i DiVA

fulltext(1063 kB)154 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 1063 kBChecksumma SHA-512
8826dd1e5d6ff70cf85954810db9aaa6eabeba25ff1fda73651c2d5975dfbcb1baaccef21ff5a54aa261d459742d92091eb49ba6d5eae707e1820b3b8ad238bb
Typ fulltextMimetyp application/pdf

Övriga länkar

Förlagets fulltextScopus

Personposter BETA

Mousavi, Mohammad Reza

Sök vidare i DiVA

Av författaren/redaktören
Mousavi, Mohammad Reza
Av organisationen
Centrum för forskning om inbyggda system (CERES)
I samma tidskrift
Electronic Communications of the EASST
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 154 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 207 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf