首页    期刊浏览 2024年12月05日 星期四
登录注册

文章基本信息

  • 标题:State Distribution Policy for Distributed Model Checking of Actor Models
  • 本地全文:下载
  • 作者:Ehsan Khamespanah ; Marjan Sirjani ; Mohammadreza Mousavi
  • 期刊名称:Electronic Communications of the EASST
  • 电子版ISSN:1863-2122
  • 出版年度:2015
  • 卷号:72
  • DOI:10.14279/tuj.eceasst.72.1022
  • 语种:English
  • 出版社:European Association of Software Science and Technology (EASST)
  • 摘要: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 the 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.
  • 其他摘要: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 the 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.
国家哲学社会科学文献中心版权所有