Action systems,unbounded nondeterminism,and infinite traces

Morgan [Mor90a] has described a correspondence between Back's action systems [BKS83] and the conventionalfailures-divergences model of Hoare'scommunicating sequential processes (CSP) formalism [Hoa85]. However, the CSP failures-divergences model does not treat unbounded nondeterminism, although unbounded nondeterminism arises quite naturally in action systems; to that extent, the correspondence between the two approaches is inadequate.Fortunately there is an extendedinfinite traces model of CSP [RoB89] which treats unbounded nondeterminism. We extend the CSP-action system correspondence, using that model instead, to take the unbounded nondeterminism of action systems properly into account.In passing, we develop a definition of the weakest precondition under which an infinite heterogeneous trace of actions is enabled.Funded by Broadcom Éireann Research Ltd, Dublin.     

Implementing atomic actions in Ada 95

Atomic actions are an important dynamic structuring technique that aid the construction of fault-tolerant concurrent systems. Although they were developed some years ago, none of the well-known commercially-available programming languages directly support their use. This paper summarizes software fault tolerance techniques for concurrent systems, evaluates the Ada 95 programming language from the perspective of its support for software fault tolerance, and shows how Ada 95 can be used to implement software fault tolerance techniques. In particular, it shows how packages, protected objects, requeue, exceptions, asynchronous transfer of control, tagged types, and controlled types can be used as building blocks from which to construct atomic actions with forward and backward error recovery, which are resilient to deserter tasks and task abortion     

Resilient Distributed Computing

A control abstraction called atomic action is a powerful general mechanism for ensuring consistent behavior of a system in spite of failures of individual computations running in the system, and in spite of system crashes. However, because of the ``all-or-nothing' property of atomic actions, an important amount of work might be abandoned needlessly when an internal error is encountered. This paper discusses how implementation of resilient distributed systems can be supported using a combination of nested atomic actions and stable checkpoints. Nested atomic actions form a tree structure. When an internal atomic action terminates, its results are not made permanent until the outermost atomic action commits, but they survive local node failures. Each subtree of atomic actions is recoverable individually. A checkpoint is established in stable storage as part of a remote request so that results of such a request can be reclaimed if the requesting node fails in the meantime, The paper shows how remote procedure call primitives with ``at-most-once' semantics and recovery blocks can be built with these mechanisms.     

Attacking Fair-Exchange Protocols: Parallel Models vs. Trace Models

Most approaches to formal protocol verification rely on an operational model based on traces of atomic actions. Modulo CSP, CCS, state-exploration, Higher Order Logic or strand spaces frills, authentication or secrecy are analyzed by looking at the existence or the absence of traces with a suitable property.We introduced an alternative operational approach based on parallel actions and an explicit representation of time. Our approach consists in specifying protocols within a logic language ( AL _SP), and associating the existence of an attack to the protocol with the existence of a model for the specifications of both the protocol and the attack.In this paper we show that, for a large class of protocols such as authentication and key exchange protocols, modeling in AL _SP is equivalent - as far as authentication and secrecy attacks are considered - to modeling in trace based models.We then consider fair exchange protocols introduced by N. Asokan et al. showing that parallel attacks may lead the trusted third party of the protocol into an inconsistent state. We show that the trace based model does not allow for the representation of this kind of attacks, whereas our approach can represent them.     

A unified algorithm to determine the reachable and dexterous workspace of parallel manipulators

This paper presents a novel idea for determining the reachable and dexterous workspace of parallel manipulators. Both the reachable workspace and dexterous workspace are utmost important for optimal design and performance comparison of manipulators, because each configuration or point in this region has specified kinematic dexterity by the designer. We propose a uniform algorithm, called stratified workspace boundary determining algorithm (SWBDA), which considers various physical and contrived constraints. The problems of determining the reachable and dexterous workspace boundaries are defined and the unified method is applied to solve all the problems of this kind. The validity and efficiency of the proposed method are verified with two kinds of representative parallel manipulator, since their relational results were studied in literatures. Finally, the advantages of the proposed method are summarized by comparing with other methods.     

Design and verification of fault tolerant systems with CSP

Summary By means of an example, we present a formal method based on CSP to design fault tolerant systems. This method combines algebraic and assertional techniques to achieve complete formal verification of the fault tolerant system's correctness properties. Verification steps are executed in parallel with top-down design, so that correctness proofs can be clearly structured and their completeness easily checked. In this way formal verification is applicable not only to small examples but to reasonably large systems. Jan Peleska was born in 1958 in Hamburg, received his Diploma in Mathematics from the University of Hamburg in 1981 and a Ph.D. in Mathematics in 1982. From 1981 to 1984 he worked in research and software development projects in the field of accoustics. Since 1984 he has been working with Philips and DST in Kiel in the field of distributed information systems. Peleska's current research interests include fault tolerant systems, distributed database systems and formal design and verification methods.     

Novel Double Modular Redundancy Based Fault-Tolerant FIR Filter for Image Denoising

In signal processing and communication systems, digital filters are widely employed. In some circumstances, the reliability of those systems is crucial, necessitating the use of fault tolerant filter implementations. Many strategies have been presented throughout the years to achieve fault tolerance by utilising the structure and properties of the filters. As technology advances, more complicated systems with several filters become possible. Some of the filters in those complicated systems frequently function in parallel, for example, by applying the same filter to various input signals. Recently, a simple strategy for achieving fault tolerance that takes advantage of the availability of parallel filters was given. Many fault-tolerant ways that take advantage of the filter’s structure and properties have been proposed throughout the years. The primary idea is to use structured authentication scan chains to study the internal states of finite impulse response (FIR) components in order to detect and recover the exact state of faulty modules through the state of non-faulty modules. Finally, a simple solution of Double modular redundancy (DMR) based fault tolerance was developed that takes advantage of the availability of parallel filters for image denoising. This approach is expanded in this short to display how parallel filters can be protected using error correction codes (ECCs) in which each filter is comparable to a bit in a standard ECC. “Advanced error recovery for parallel systems,” the suggested technique, can find and eliminate hidden defects in FIR modules, and also restore the system from multiple failures impacting two FIR modules. From the implementation, Xilinx ISE 14.7 was found to have given significant error reduction capability in the fault calculations and reduction in the area which reduces the cost of implementation. Faults were introduced in all the outputs of the functional filters and found that the fault in every output is corrected.     

Fault estimation observer design for a class of nonlinear multiagent systems in finite‐frequency domain

This paper focuses on the fault estimation observer design problem in the finite‐frequency domain for a class of Lipschitz nonlinear multiagent systems subject to system components or actuator fault. First, the relative output estimation error is defined based on the directed communication topology of multiagent systems, and an observer error system is obtained by connecting adaptive fault estimation observer and the state equation of the original system. Then, sufficient conditions for the existence of the fault estimation observer are obtained by using a generalized Kalman‐Yakubovich‐Popov lemma and properties of the matrix trace, which guarantee that the observer error system satisfies robustness performance in the finite‐frequency domain. Meanwhile, the pole assignment method is used to configure the poles of the observer error system in a certain area. Finally, the simulation results are presented to illustrate the effectiveness of the proposed method.     

并行分布式计算机样机的监测测试

介绍了一个基于联机实时监测的方案,它采用了作者研制的ＭＳ－１监测系统。该系统是一个具有同步实时时钟的分布式监测系统,采用事件驱动的软硬件混合监测方式,联机实时监测软件ＯＭ把监测系统的控制与监测数据的采集和观测分析结合起来,完成了联机监测与分析,用来及时提供系统的内部状态信息和动态行为。     

Introducing extra operations in refinement

This paper reconsiders refinements which introduce actions on the concrete level which were not present at the abstract level. It considers a range of different basic refinement relations, covering the standard ones for formalisms like Event-B, Z, action systems, and CSP. It also describes a number of ways in which new operations may be introduced: extended interfaces, internal actions, stuttering steps, and action refinement. The main contribution of this paper is in exploring the interaction between those two dimensions. In particular, it shows how the “refining skip” method is incompatible with failures-based refinement relations, and consequently some decisions in designing Event-B refinement are more entangled than previously highlighted.     

Event refinement in state-based concurrent systems

Operations on action systems may be defined corresponding to CSP hiding and renaming. These are of particular use in describing the refinement between action systems in which the granularity of actions is altered. We derive a simplified expression for hiding sets of actions and present sufficient conditions for forwards simulation in which the concrete system uses hiding and renaming. Both of these reduce the complexity of proofs of refinement. We present a case study in specification and refinement using action systems which makes use of the operations and refinement rules previously defined.A trademark of the IBM Corporation.     

Learning Atomic Human Actions Using Variable-Length Markov Models

Visual analysis of human behavior has generated considerable interest in the field of computer vision because of its wide spectrum of potential applications. Human behavior can be segmented into atomic actions, each of which indicates a basic and complete movement. Learning and recognizing atomic human actions are essential to human behavior analysis. In this paper, we propose a framework for handling this task using variable-length Markov models (VLMMs). The framework is comprised of the following two modules: a posture labeling module and a VLMM atomic action learning and recognition module. First, a posture template selection algorithm, based on a modified shape context matching technique, is developed. The selected posture templates form a codebook that is used to convert input posture sequences into discrete symbol sequences for subsequent processing. Then, the VLMM technique is applied to learn the training symbol sequences of atomic actions. Finally, the constructed VLMMs are transformed into hidden Markov models (HMMs) for recognizing input atomic actions. This approach combines the advantages of the excellent learning function of a VLMM and the fault-tolerant recognition ability of an HMM. Experiments on realistic data demonstrate the efficacy of the proposed system.     

A graphic modeling and analysis tool for human fault diagnosis tasks

This study presents a graphic modeling and analysis tool for use in constructing an operator's mental model in fault diagnosis tasks. In most automatic and complicated process control systems, human fault diagnosis tasks have become increasingly complex and specialized. The system designer should consider the cognitive process of human operator to avert failure of implement action owing to a lack of compatibility between humans and aiding system interface. Here, an experiment is performed to investigate the nature of human fault diagnosis. A graphic modeling and analysis tool is then proposed to model the continuous process of human fault diagnosis. The approach proposed herein exploits both the line-chart and Petri nets to demonstrate the operator's thoughts and actions. Moreover, results in this study are integrated into an adaptive standard diagnosis model that can assess the operators' mental workload and accurately depict the interactions between human operator and aiding system.Relevance to industryAutomatic intelligent diagnosis systems can not provide satisfactory operating performance. Human diagnosticians are more effective than computer ones. Results in this study offer further insight into an operator behavior in graphic form and also how to design a better aiding system.     

Using coordinated atomic actions to design safety‐critical systems: a production cell case study

Coordinated Atomic actions (CA actions) are a unified approach to structuring complex concurrent activities and supporting error recovery between multiple interacting objects in object‐oriented systems. This paper explains how we have used the CA action concept to design and implement a safety‐critical application. We have used the Production Cell model that was developed in the Forschungszentrum Informatik (FZI), Karlsruhe, Germany, to present a realistic industry‐oriented problem, where safety requirements play a significant role. Our design consists of two levels: the first level deals with the scheduling of CA actions, and the second level deals with the interactions between devices. Both the scheduling mechanism and the device interactions are enclosed by CA actions. Exception handling and error recovery are incorporated into CA actions in order to satisfy high safety and fault tolerance requirements. A controlling program based on our design was developed in the Java language and used to drive a graphical simulator provided by the FZI. Copyright © 1999 John Wiley & Sons, Ltd.     

基于Storm的局部放电信号集合经验模态分解

电力设备的稳定运行关系到人们的生命和财产安全,通过安装传感器对时序波形信号进行采集,对信号进行分析处理,可以实现对电力设备的故障诊断。集合经验模态分解（Ensemble Empirical Mode Decomposition,EEMD）算法在非线性、非平稳的信号处理领域有其独特的优势,但是由于其算法复杂度较大,作为运算密集型的算法在串行执行的情况下运算速度无法满足实际需求。因此,借助分布式计算框架Storm并行处理的特点,提出了基于Storm的EMD过程并行和信号分段并行的两种EEMD分解方式。实验表明,两种并行化方案都比传统的串行执行方式速度更快,并且基于分段并行的方式由于其更高的并行度,在长信号处理中更具优势。两种并行EEMD算法的提出为时序信号的快速处理提供了可靠的解决方案。     

基于混合动态主元分析的故障检测方法

针对基于动态主元分析的故障检测方法存在的主元个数较多以及计算效率低等问题,本文提出基于混合动态主元分析(Hybrid Dynamic Principal Component Analysis,HDP-CA)的复杂过程故障检测方法。该方法采用分步策略消除数据之间的自相关和互相关性,提高了故障检测的精度和效率。对TE过程典型故障和热连轧过程中断带故障检测结果表明:HDPCA方法提取的主元个数少于DPCA方法提取的主元个数。并且,基于HDPCA的T2和SPE统计量的检测性能和检测精度都由于基于DPCA的统计量。因此,本文提出的方法可以准确有效地检测出故障。     

A fault-injection methodology for the system-level dependability analysis of multiprocessor embedded systems

This paper presents a methodology for the system-level dependability analysis of multiprocessor embedded systems. The methodology is based on fault injection and features an error analysis approach offering to the designer the possibility to specify custom monitoring and classification actions at both application and architecture levels. In particular, a debug-like mechanism offers the possibility to interpret architectural raw data observed during the simulation at application level with a function call/return granularity, thus offering the possibility to analyze the propagation of the errors in the various functionalities of the executed application. A framework for automating the proposed methodology has been implemented within a state-of-the-art SystemC/TLM simulation platform for multiprocessor specifications provided with a fault injection engine. The effectiveness of the methodology has been demonstrated in two different case studies, showing how the proposed approach is able to produce an accurate dependability report highlighting the criticalities in both the architecture and the application of the system under design.     

Structural characterization of deformed crystals by analysis of common atomic neighborhood

Simulations of crystal deformation and structural transformation may generate complex datasets involving networks with million to billion chemical bonds which makes local structure analysis a challenge. An ideal analysis method must recognize perfect crystal structures, such as face-centered cubic, body-centered cubic and hexagonal close packed, and differentiate structural defects such as dislocations, stacking faults, grain boundaries, cracks and surfaces. Currently a few methods are used for this purpose, e.g., the Common Neighbor Analysis (CNA) and the Centrosymmetry Parameter (CSP). This paper proposes an alternative method based on the calculation of a single parameter that depends on the common atomic neighborhood. We validate the method characterizing local structures in complex molecular-dynamics datasets, clarifying its advantages over the CNA and the CSP methods.     

Fault-Tolerant Recursive Least-Squares Computations on a Mesh-Connected Parallel Processor

Recursive least squares (RLS) is a popular iterative method used for the modeling of systems while in operation. RLS provides an estimate for unknown parameters of a system based on some known parameters and inputs and outputs of that system. This technique is used frequently in digital signal processing and control applications, where it is not possible to completely determine the current state of the system. The RLS procedure incurs intensive computations in every iteration of the algorithm. To implement RLS in situ at a reasonable sampling rate, the complexity of the system's model must be reduced, or the available computing power must be increased. This paper examines methods for increasing the computing power by implementing RLS algorithms on a parallel processing platform. While there has been a large body of research on using parallel processors for the computation of adaptive algorithms, little of this research has examined fault tolerant aspects. As fault tolerance is a critical aspect of any real-time system, this work will examine some factors that should be considered when implementing a real-time adaptive algorithm on a parallel processor system.