Compositional and local livelock analysis for CSP
Compositional and local livelock analysis for CSP
复制标题
DOI：
10.1016/j.ipl.2017.12.011
复制
发表时间：
2018-05-01
影响因子：
0.5
通讯作者：
Cavalcanti, Ana
中科院分区：
文献类型：
--
作者：
Conserva Filho, M. S.;Oliveira, M. V. M.;Cavalcanti, Ana
基于组件的软件构建技术的成功依赖于对组合的紧急行为的信任。在这里，我们提出了一种高效的无活锁CSP模型的纠错构造技术。其验证条件基于对代表CSP模型中的递归行为的最短事件序列(轨迹)的本地分析。这显著提高了模型检查的性能。我们基于米尔纳的调度器和餐饮哲学家的模型来评估我们的策略。(C)2018爱思唯尔B.V.保留所有权利。
The success of component-based techniques for software construction relies on trust in the emergent behaviour of the compositions. Here, we propose an efficient correct-by construction technique for building livelock-free CSP models. Its verification conditions are based on a local analysis of the shortest event sequences (traces) that represent a recursive behaviour in the CSP model. This affords significant gains in performance in model checking. We evaluate our strategy based on models of the Milner's scheduler and the dining philosophers. (C) 2018 Elsevier B.V. All rights reserved.