Tyck till om SwePub Sök
här!
Sökning: WFRF:(Mousavi Mohammad Reza 1978 )
> (2015-2019)
> Sabahi Kaviani Zeynab >
State Distribution ...
-
Khamespanah, EhsanUniversity of Tehran, School of Electrical and Computer Engineering, Tehran, Iran & Reykjavik University, School of Computer Science, Reykjavik, Island
(författare)
State Distribution Policy for Distributed Model Checking of Actor Models
- Artikel/kapitelEngelska2015
Förlag, utgivningsår, omfång ...
-
Berlin :Universitätsverlag der TU Berlin,2015
-
electronicrdacarrier
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:hh-29997
-
https://urn.kb.se/resolve?urn=urn:nbn:se:hh:diva-29997URI
-
https://doi.org/10.14279/tuj.eceasst.72.1022.1011DOI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:ref swepub-contenttype
-
Ämneskategori:art swepub-publicationtype
Anmärkningar
-
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.
-
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.
Ämnesord och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Sirjani, MarjanReykjavik University, School of Computer Science, Reykjavik, Island
(författare)
-
Mousavi, Mohammad Reza,1978-Högskolan i Halmstad,Centrum för forskning om inbyggda system (CERES)(Swepub:hh)mohmou
(författare)
-
Sabahi Kaviani, ZeynabUniversity of Tehran, School of Electrical and Computer Engineering, Tehran, Iran
(författare)
-
Razzazi, Mohammad RezaAmirkabir University of Technology, School of Computer Engineering and Information Technology, Tehran, Iran
(författare)
-
University of Tehran, School of Electrical and Computer Engineering, Tehran, Iran & Reykjavik University, School of Computer Science, Reykjavik, IslandReykjavik University, School of Computer Science, Reykjavik, Island
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:Electronic Communications of the EASSTBerlin : Universitätsverlag der TU Berlin72, s. 1-151863-2122
Internetlänk
Hitta via bibliotek
Till lärosätets databas