Specification and Modelling of Fault Tolerant and Self Healing Systems Visiting Fellowship for Professor Tom Maibaum

如果一个系统可以在没有外部干预的情况下从故障中恢复，那么它就被称为自我修复。换句话说，系统能够在部分故障后自动重组以继续运行。这显然与容错的概念密切相关，在容错的概念中，系统可以在经历故障的情况下正常运行。我们使用术语自我修复来表示比通常用术语容错表示的更广泛的系统类别和重组程度。这项建议是为了使帝国理工学院的分布式软件工程(DSE)小组能够了解和应用Tom Maibaum教授开发的描述和推理技术。特别值得一提的是，迈鲍姆教授是国际上的情态动作逻辑专家。这些逻辑可以允许形式化地指定良好行为和异常行为的概念，从而允许对容错进行精确的推理。我们打算研究它们在自我修复系统中的应用，这些系统可以根据环境的变化进行动态重新配置。DSE有一个现有的工具集，称为标记的转换系统分析器(LTSA)，它允许使用进程代数概念来指定一组系统组件的行为。此外，可以机械地检查组件的组成，以表明它们满足某些精确指定的属性。然而，目前，虽然一些自我修复的概念可以在LTSA中表达，但这是繁琐的，并且可以检查的属性与自我修复没有明显或直接的关系。因此，该项目的目标是利用Maibaum教授的工作，对自我修复系统及其必须满足的特性进行简洁的说明。

A system is said to be self-healing if it can recover from failures without external intervention. In other words, the system is capable of automatically re-organising itself to continue operating after part of it has failed. This is obviously closely related to the notion of fault-tolerance in which a system can operate normally despite experiencing failures. We use the term self-healing to mean a wider class of systems and degree of re-organization than is usually denoted by the term fault-tolerant.This proposal is to enable the Distributed Software Engineering (DSE) group at Imperial College to learn about and apply the description and reasoning techniques developed by Professor Tom Maibaum. In particular, Professor Maibaum is an international expert in modal action logics. These logics can allow notions of good behaviour and abnormal behaviour to be formally specified and as a result permit precise reasoning about fault tolerance. We intend to look at their application in self-healing systems which can dynamically reconfigure in response to changes in their environment.DSE has an existing toolset called the Labelled Transition System Analyser (LTSA) which permits the behaviour of a set of systems components to be specified using a process algebra notion. In addition, a composition of components can be mechanically checked to show that they satisfy certain precisely specified properties. However, currently, while some notions of self-healing can be expressed in the LTSA, this is cumbersome and the properties that can be checked not obviously or directly related to self-healing. The objectives of this project are thus to use Professor Maibaum's work to allow the succinct specification of both self-healing systems and the properties that they must satisfy.