首页> 外文期刊>Science of Computer Programming >Actor-based slicing techniques for efficient reduction of Rebeca models
【24h】

Actor-based slicing techniques for efficient reduction of Rebeca models

机译:基于Actor的切片技术可有效简化Rebeca模型

获取原文
获取原文并翻译 | 示例

摘要

Slicing is a program analysis technique which can be used for reducing the size of the model and avoid state space explosion in model checking. In this work a static slicing technique is proposed for reducing Rebeca models with respect to a property. For applying the actor-based slicing techniques, the Rebeca control flow graph (RCFG) and the Rebeca dependence graph (RDG) are introduced. We propose two different approaches for constructing the RDC, where each approach can be more effective under certain conditions. As the static slicing usually produces large slices, two other slicing-based reduction techniques, step-wise slicing and bounded slicing, are proposed as simple novel ideas. Step-wise slicing first generates slices that overapproximate the behavior of the original model and then refines it, and bounded slicing is based on the semantics of nondeterministic assignments in Rebeca. We also propose a static slicing algorithm for deadlock detection (in absence of any particular property). The efficiency of these techniques is checked by applying them to several case studies which are included in this paper. Similar techniques can be applied on the other actor-based languages.
机译:切片是一种程序分析技术,可用于减小模型的大小并避免在模型检查中出现状态空间爆炸。在这项工作中,提出了一种静态切片技术来减少关于属性的Rebeca模型。为了应用基于角色的切片技术,引入了Rebeca控制流图(RCFG)和Rebeca依赖图(RDG)。我们提出了两种不同的构建RDC的方法,其中每种方法在某些条件下可能更有效。由于静态切片通常会产生较大的切片,因此提出了另外两种基于切片的归约技术(逐步切片和有界切片)作为简单新颖的思想。逐步切片首先生成使原始模型的行为过分逼近的切片,然后对其进行细化,然后有界切片基于Rebeca中非确定性分配的语义。我们还提出了一种用于死锁检测的静态切片算法(在没有任何特定属性的情况下)。通过将这些技术应用于本文中包含的几个案例研究,可以检验这些技术的效率。类似的技术可以应用于其他基于参与者的语言。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号