Specification and Analysis of Fault Behaviours Using Graph Grammars
Specification and Analysis of Fault Behaviours Using Graph Grammars
复制标题
使用图文法对故障行为进行规范和分析
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
O. M. Santos
中科院分区：
文献类型：
--
作者：
F. Dotti;L. Ribeiro;O. M. Santos
在本文中，我们使用形式化的方法和工具作为手段来指定和推理分布式系统在存在故障时的行为。所使用的方法是基于这样一种观察，即故障行为可以被建模为系统不需要但可能发生的过渡。然后，就有可能定义将分布式系统的模型m1转换为模型m2，该模型m2表示存在选定故障时原始系统的行为。我们使用一种称为基于对象的图形语法的形式化规范语言来描述异步分布式系统的模型，并为用这种语言编写的模型提供了引入一组经典故障模型的转换步骤，这些模型可以在文献中找到。作为这个过程的结果，在转换后的模型上，开发人员可以在选择错误行为的情况下推断出原始模型的行为。作为案例研究，我们提出了基于拉的故障检测器的规范，然后将该模型转换为包括碰撞故障模型的行为，并通过仿真分析了存在碰撞时基于拉的故障检测器的行为。
In this paper we make use of formal methods and tools as means to specify and reason about the behavior of distributed systems in the presence of faults. The approach used is based on the observation that a fault behavior can be modeled as an unwanted but possible transition of a system. It is then possible to define a transformation of a model M 1 of a distributed system into a model M 2 representing the behavior of the original system in the presence of a selected fault. We use a formal specification language called Object Based Graph Grammars to describe models of asynchronous distributed systems and present, for models written in terms of this language, the transformation steps for introducing a set of classical fault models found in the literature. As a result of this process, over the transformed model(s) it is possible for the developer to reason about the behavior of the original model(s) in the presence of a selected fault behavior. As a case study, we present the specification of a pull-based failure detector, then we transform this model to include the behavior of the crash fault model and analyze, through simulation, the behavior of the pull-based failure detector in the presence of a crash.