Diagnosis of Active Systems by Automata-Based Reasoning Techniques

This paper presents a method for the diagnosis of active systems, these being a class of distributed asynchronous discrete-event systems, such as digital networks, communication networks, and power transmission protection systems. Formally, an active system is viewed as a network of communicating automata, where each automaton describes the behavior of a system component. The diagnostic method encompasses four steps, namely system modeling, reconstruction planning, behavior reconstruction, and diagnosis generation. System modeling formally defines the structure and behavior of system components, as well as the topology of the active system. Based on optimization criteria, reconstruction planning breaks down the problem of system behavior reconstruction into a hierarchical decomposition. Behavior reconstruction yields an intensional representation of all the dynamic behaviors that are consistent with the available system observation. Eventually, diagnosis generation extracts diagnostic information from the reconstructed behaviors. The diagnostic method is applied to a case study in the power transmission network domain. Unlike other proposals, our approach both deals with asynchronous events and does not require any global diagnoser to be built off-line. The method, which is substantiated by an ongoing implementation, is scalable, incremental, and amenable to parallelism, so that real size problems can be handled.     

一种结合时间区间代数建模的主动系统的故障诊断方法

研究了在全局时钟、线性观测、串行事件触发的主动系统的故障诊断,在原有主动系统的自动机建模的基础上,引入时间区间代数表达更为详细的时间约束信息,构成带有时间的自动机对系统组件建模;同样在所得观测中也加入相应的更为详细的时间信息.由于加上了时间的约束,可使得诊断的解释空间进一步缩小,从而在一定情况下可提高诊断效率.最后讨论了非线性不确定观测或并发等一般情形下的处理方法.     

A bridged diagnostic method for the monitoring of polymorphic discrete-event systems.

Diagnosis of discrete-event systems (DESs) is a challenging problem that has been tackled both by automatic control and artificial intelligence communities. The relevant approaches share similarities, including modeling by automata, compositional modeling, and model-based reasoning. This paper aims to bridge two complementary approaches from these communities, namely, the diagnoser approach and the active system approach, respectively. The more significant shortcomings of such approaches are, on the one side, the need for the generation of the global system model and, on the other, the lack of monitoring capabilities. The former makes the application of the diagnoser approach prohibitive in real contexts, where the system model is too large to be generated, even offline. The latter requires the completion of the system observation before starting the diagnostic task, thereby, making the monitoring of the system. impossible. The bridged diagnostic method subsumes, to a large extent on the peculiarities of the two approaches and is capable of coping with an extended class of DESs that integrate both synchronous and asynchronous behavior. The bridge is built by extending the active system approach by means of several enhanced techniques, which eventually, allow the efficient monitoring of polymorphic DESs. Upon the occurrence of each system message, two pieces of diagnostic information are generated, namely, the snapshot and historic diagnostic sets. While the former accounts for the faults pertinent to the newly generated message only, the latter is based on the whole sequence of messages yielded by the system during operation.     

基于迁移系统分析的线性混成系统安全验证

混成自动机行为中既包含离散行为又包含连续行为,非常复杂。其安全性验证问题难以解决,即使是线性混成自动机,它的可达性问题也被证明是不可判定的。现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集,复杂度高,可处理问题规模非常有限。为了避免这类问题,实现了一种新的工具。该工具将线性混成自动机表达为等价的迁移系统,并利用迁移系统上不变式生成相关工作对混成自动机进行验证。实验数据表明,方法有效可行,工具具有良好的性能。     

<Emphasis Type="Italic">SetExp</Emphasis>: a method of transformation of timed automata into finite state automata

Real-time discrete event systems are discrete event systems with timing constraints, and can be modeled by timed automata. The latter are convenient for modeling real-time discrete event systems. However, due to their infinite state space, timed automata are not suitable for studying real-time discrete event systems. On the other hand, finite state automata, as the name suggests, are convenient for modeling and studying non-real time discrete event systems. To take into account the advantages of finite state automata, an approach for studying real-time discrete event systems is to transform, by abstraction, the timed automata modeling them into finite state automata which describe the same behaviors. Then, studies are performed on the finite state automata model by adapting methods designed for non real-time discrete event systems. In this paper, we present a method for transforming timed automata into special finite state automata called Set-Exp automata. The method, called SetExp, models the passing of time as real events in two types: Set events which correspond to resets with programming of clocks, and Exp events which correspond to the expiration of clocks. These events allow to express the timing constraints as events order constraints. SetExp limits the state space explosion problem in comparison to other transformation methods of timed automata, notably when the magnitude of the constants used to express the timing constraints are high. Moreover, SetExp is suitable, for example, in supervisory control and conformance testing of real-time discrete event systems.     

A Supervisory Control Method for Ensuring the Conformance of Real-Time Discrete Event Systems

In this article, we study the problem of controlling a plant described as a real-time discrete event system. The aimed objective is to ensure a conformance relation denoted tioco between the plant and the formal specification of the system, by means of a supervisor. We adopt a two-step approach. In Step 1, we express the problem into a non-real-time form, by using a transformation of timed automata (TA) into particular finite state automata called Set-Exp-Automata (SEA). The latter use two additional types of events, Set and Exp. And in Step 2, we propose a non-real-time control method suitable for SEA. We also propose a control architecture.     

绿色网络存储系统的动力学分析模型

分析和研究了复杂网络存储系统中能耗管理控制的动力学行为规律。通过分析网络存储系统中的磁盘能耗模型,提出一种针对分布式网络存储系统的理想化能耗优化数据布局模型(IEEDP)。在此基础上,结合数据迁移和数据复制技术,提出一种基于二维元胞自动机的绿色网络存储系统模型(GNSSCA)。实验表明,通过节点的局部性调节行为,该系统呈现出复杂的时空演化现象。系统总体副本个数随着负载的增加而出现相应的增加并最终趋于稳定。在负载较低的情况下,节点的访问队列长度嫡出现近似的幂律分布。     

Diagnosis of timed automata: Theory and application to the DAMADICS actuator benchmark problem

This paper concerns the problem of fault diagnosis in discrete-event systems which are represented by timed automata. The diagnostic algorithm for timed automata detects and identifies faults in the system based on the investigation whether the measured input and output sequences are consistent with the timed automaton. This diagnostic approach can be applied spontaneously to the discrete-event system since no a priori information about the initial state of the system is required. It is shown in the paper how the timed automaton which represents the DAMADICS actuator can be obtained and how the diagnostic algorithm based on the timed automaton is applied to detect and identify actuator faults. A representative diagnostic result is presented and discussed to illustrate the effectiveness of the method.     

Discrete Semantics for Hybrid Automata

Many natural systems exhibit a hybrid behavior characterized by a set of continuous laws which are switched by discrete events. Such behaviors can be described in a very natural way by a class of automata called hybrid automata. Their evolution are represented by both dynamical systems on dense domains and discrete transitions. Once a real system is modeled in a such framework, one may want to analyze it by applying automatic techniques, such as Model Checking or Abstract Interpretation. Unfortunately, the discrete/continuous evolutions not only provide hybrid automata of great flexibility, but they are also at the root of many undecidability phenomena. This paper addresses issues regarding the decidability of the reachability problem for hybrid automata (i.e., “can the system reach a state a from a state b?”) by proposing an “inaccurate” semantics. In particular, after observing that dense sets are often abstractions of real world domains, we suggest, especially in the context of biological simulation, to avoid the ability of distinguishing between values whose distance is less than a fixed ε. On the ground of the above considerations, we propose a new semantics for first-order formulæ which guarantees the decidability of reachability. We conclude providing a paradigmatic biological example showing that the new semantics mimics the real world behavior better than the precise one.     

Emergence of conventions through social learning

Societal norms or conventions help identify one of many appropriate behaviors during an interaction between agents. The offline study of norms is an active research area where one can reason about normative systems and include research on designing and enforcing appropriate norms at specification time. In our work, we consider the problem of the emergence of conventions in a society through distributed adaptation by agents from their online experiences at run time. The agents are connected to each other within a fixed network topology and interact over time only with their neighbours in the network. Agents recognize a social situation involving two agents that must choose one available action from multiple ones. No default behavior is specified. We study the emergence of system-wide conventions via the process of social learning where an agent learns to choose one of several available behaviors by interacting repeatedly with randomly chosen neighbors without considering the identity of the interacting agent in any particular interaction. While multiagent learning literature has primarily focused on developing learning mechanisms that produce desired behavior when two agents repeatedly interact with each other, relatively little work exists in understanding and characterizing the dynamics and emergence of conventions through social learning. We experimentally show that social learning always produces conventions for random, fully connected and ring networks and study the effect of population size, number of behavior options, different learning algorithms for behavior adoption, and influence of fixed agents on the speed of convention emergence. We also observe and explain the formation of stable, distinct subconventions and hence the lack of emergence of a global convention when agents are connected in a scale-free network.     

Specifying and verifying contract-driven service compositions using commitments and model checking

The paper proposes a novel model checking-based approach towards verifying the compliance of intelligent agent-based web services with contracts regulating their compositions specified in the Business Process Execution Language (BPEL). Unlike the existing approaches in the literature, the main contribution and impact of the introduced approach is the ability to verify intelligent and autonomous composite web services by capturing and describing in details both compliance and violation behaviors, how the system can distinguish between them, and how the system reacts and can be recovered after each violation. The approach encompasses three contributing parts, namely: 1) the marking process of an extended BPEL; 2) the transformation of the extended and marked BPEL to an automata model; and 3) the encoding of the resulting automata model into the Interpreted Systems Programming Language (ISPL), the input language of the MCMAS model checker for intelligent and autonomous multi-agent systems. In the first part, we extend BPEL that specifies the business process of the composition by creating custom activities called labels. We use those labels as means to represent the specifications and mark the points the developer aims to verify. A significant advantage of this labeling is the ability to highlight specific points in the design to be verified and to distinguish compliance behaviors from violations, which makes this verification focused and highly efficient. In the second part, we introduce new transformation rules to transform the extended and marked BPEL to an automata model. This transformation requires a prior modeling of agent-based web services composition using automata definitions. In the third part, we introduce algorithmic translation rules encoding the resulting automata model into ISPL. This translation makes model checking the behavior of our contract-driven compositions possible. A novel characteristic of the proposed approach is the automatic generation of the properties against which the system is verified from the composition’s implementation, which is technically challenging. The verification properties are expressed in the Computation Tree Logic of Commitments (CTLC). Technically, CTLC provides a powerful representation to formally model 1) interactions among multi-agent based web services and 2) compliance and violation behaviors within composite business contracts by making use of communicative commitment operators. CTLC also includes a fulfillment operator which helps formally check the compliance with business contracts and specify the system recovery. A detailed case study from expert and intelligent systems domain along with experimental results are also reported in the paper. Finally, the main impact and significance of the paper on expert and intelligent systems is the ability to use these systems safely since there is a way to verify if the intelligent components behave according to and in compliance with the underlying regulating contracts.     

On the history of diagnosability and opacity in discrete event systems

This paper presents historical remarks on key projects and papers that led to the development of a theory of event diagnosis for discrete event systems modeled by finite-state automata or Petri nets in the 1990s. The goal in event diagnosis is to develop algorithmic procedures for deducing the occurrence of unobservable events, based on a formal model of the system and on-line observations of its behavior. It also presents historical remarks on the early works on the property of opacity, which occurred about ten years later. Opacity can be seen as a strong version of lack of diagnosability and it has been used to capture security and privacy requirements. Finally, diagnosability is connected with the property of observability that arises in supervisory control. This paper is part of set of papers that review the emergence of discrete event systems as an area of research in control engineering.     

Ethernet based time synchronization for Raspberry Pi network improving network model verification for distributed active turbulent flow control

Friction drag primarily determines the total drag of transport systems. A promising approach to reduce drag at high Reynolds numbers(> 104) are active transversal surface waves in combination with passive methods like a riblet surface. For the application in transportation systems with large surfaces such as airplanes, ships or trains, a large scale distributed real-time actuator and sensor network is required. This network is responsible for providing connections between a global flow control and distributed actuators and sensors. For the development of this network we established at first a small scale network model based on Simulink and True Time. To determine timescales for network events on different package sizes we set up a Raspberry Pi based testbed as a physical representation of our first model. These timescales are reduced to time differences between the deterministic network events to verify the behavior of our model. Experimental results were improved by synchronizing the testbed with sufficient precision. With this approach we assure a link between the large scale model and the later constructed microcontroller based real-time actuator and sensor network for distributed active turbulent flow control.     

基于动态观测的随机离散事件系统故障诊断

近年来,离散事件系统故障诊断研究引起国内外学者广泛关注.鉴于此,研究动态观测下随机离散事件系统的故障诊断.首先引入一种动态观测,使事件的可观测性随着系统的运行而动态变化;然后分别对基于动态观测的随机离散事件系统的单故障可诊断性和模式故障可诊断性进行形式化;最后通过构造相应的诊断器,分别得到关于单故障可诊断性和模式故障可...     

面向复杂网络存储系统的元胞自动机动力学分析方法

大规模网络存储系统中复杂的数据传输行为隐藏着一定的动力学规律性.针对基于对象的大规模网络存储系统,结合存储对象的智能性和主动性特征,分别在宏观与微观两个层次上提出了用于复杂网络存储动态行为规律分析的存储元胞自动机模型SNCA和OSDCA.在SNCA模型中,对网格拓扑结构的存储网络,结合存储对象的生命周期属性,可在宏观上分析网络存储系统的数据流动规律,确定存储网络拥塞程度,仿真结果揭示数据对象流动和存储网络中的相变具有全局相关性;在OSDCA模型中,综合热点数据的迁移和复制机制,在微观上分析I/O负载动态分布特性和存储热点迁移规律,仿真结果表明对象存储系统中的数据分布具有一定的自组织特性.     

数据库活动监控工具的接口自动机模型

使用接口自动机描述软件各模块的内、外部行为,依据接口自动机的构件组合方法来描述总体框架的运行机制,可清晰地展示出基于网络嗅探的数据库活动监控工具的多DBMS协议分析支持、分布式部署与协同工作等难点的解决。给出了该工具主要模块的内、外部行为和工具整体行为的接口自动机模型,通过实验,验证了基于该模型所实现工具的正确性和可用性。     

Emergence and control of macro-spatial structures in perturbed cellular automata, and implications for pervasive computing systems

Predicting the behavior of complex decentralized pervasive computing systems before their deployment in a dynamic environment, as well as being able to influence and control their behavior in a decentralized way, will be of fundamental importance in the near future. In this context, this paper describes the general behavior observed in a large set of asynchronous cellular automata when external perturbations influence the internal activities of cellular automata cells. In particular, we observed that stable macrolevel spatial structures emerge from local interactions among cells, a behavior that does not emerge when cellular automata are not perturbed. Similar sorts of macrolevel behaviors are likely to emerge in the context of pervasive computing systems and need to be studied, controlled, and possibly fruitfully exploited. On this basis, the paper also reports the results of a set of experiments, showing how it is possible to control, in a decentralized way, the behavior of perturbed cellular automata, to make any desired patterns emerge.     

Template languages for fault monitoring of timed discrete eventprocesses

This paper introduces a new framework for modeling discrete event processes. This framework, called condition templates, allows the modeling of processes in which both single-instance and multiple-instance behaviors are exhibited concurrently. A single-instance behavior corresponds to a trace from a single finite-state process, and a multiple-instance behavior corresponds to the timed interleavings of an unspecified number of identical processes operating at the same time. The template framework allows the modeling of correct operation for systems consisting of concurrent mixtures of both single and multiple-instance behaviors. This representation can then be used in online fault monitoring for confirming the correct operation of a system. We compare the class of timed languages representable by template models with classes of timed languages from timed automata models. It is shown that templates are able to model timed languages corresponding to single and multiple-instance behaviors and combinations thereof. Templates can thus represent languages that could not be represented or monitored using timed automata alone     

模型检测基于概率时间自动机的反例产生研究

模型检测基于概率系统的反例产生问题,在最近引起人们的关注.已有的工作主要围绕模型检测Markov链的反例产生而开展.基于概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展.关注的是模型检测PTA的反例产生问题.首先通过在PTA上寻找概率之和恰好大于λ的κ条最大概率的路径,并根据这些路径和原PTA构造原PTA的一个子图,从而快速找到违背性质的具有较少证据的反例.然后精化此结果——通过逐条加入上述各条最大概率的路径来精确地计算已加入路径所构成的PTA子图的最大概率.由于考虑到符号状态交集对概率系统的影响,可以得到证据更少的反例.     

Ptolemy离散事件模型形式化验证方法

Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.本文提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件,时间自动机模型能够表达这个特征,因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义,其次设计了一组从离散事件模型到时间自动机的映射规则.然后在Ptolemy环境中实现了一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用Uppaal验证内核完成验证.最后以一个交通信号灯控制系统为例进行了成功的转换和验证,实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.