Verification of Modular Diagnosability With Local Specifications for Discrete-Event Systems

Date

2013-09-01

Author

Schmidt, Klaus Verner

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

343
views

0
downloads

In this paper, we study the diagnosability verification for modular discrete-event systems (DESs), i.e., DESs that are composed of multiple components. We focus on a particular modular architecture, where each fault in the system must be uniquely identified by the modular component where it occurs and solely based on event observations of that component. Hence, all diagnostic computations for faults to be detected in this architecture can be performed locally on the respective modular component, and the obtained diagnosis information is only relevant for that component. We define the condition of modular language diagnosability with local specifications (MDLS) in order to capture that each fault can indeed be detected in this modular architecture. Then, we show that MDLS can be formulated as a specific language-diagnosability problem. As the main contribution of this paper, we develop an incremental abstraction-based approach for the verification of MDLS, which is based on projections that fulfill the loop-preserving observer condition. In particular, our approach efficiently avoids the construction of a global system model, which is infeasible for systems of realistic size. Furthermore, we do not rely on the assumption of a live global plant, which is prevalent in previous diagnosability methods for modular DESs. We illustrate our approach and its computational savings by a manufacturing system example.

Subject Keywords

Control and Systems Engineering, Human-Computer Interaction, Electrical and Electronic Engineering, Software, Computer Science Applications

URI

https://hdl.handle.net/11511/34393

Journal

IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS

DOI

https://doi.org/10.1109/tsmca.2012.2227251

Collections

Department of Electrical and Electronics Engineering, Article

Suggestions

OpenMETU
Core

A finite field framework for modeling, analysis and control of finite state automata Reger, Johann; Schmidt, Klaus Verner (Informa UK Limited, 2004-09-01) In this paper, we address the modeling, analysis and control of finite state automata, which represent a standard class of discrete event systems. As opposed to graph theoretical methods, we consider an algebraic framework that resides on the finite field F-2 which is defined on a set of two elements with the operations addition and multiplication, both carried out modulo 2. The key characteristic of the model is its functional completeness in the sense that it is capable of describing most of the finite st...
Exhaustive study on the commutativity of time-varying systems KÖKSAL, MUHAMMET (Informa UK Limited, 1988-5) This paper, which is a survey and a compact reference on the commutativity of time-varying systems, gives the complete set of necessary and sufficient commutativity conditions for systems of any order. Original results are derived on Euler's systems, and explicit commutativity conditions are presented for fourth-order systems, which have not yet appeared in the literature.
System identification with generalized orthonormal basis functions: an application to flexible structures Nalbantoglu, V; Bokor, J; Balas, G; Gaspar, P (Elsevier BV, 2003-03-01) This paper presents an application of a multi-input/multi-output identification technique based on system-generated orthonormal basis functions to a flexible structure. A priori information about the poles of the system, part of which corresponds to the natural frequencies of the structure, is used to generate the orthonormal basis functions. A multivariable model is identified for the experimental flexible structure by using these orthonormal basis functions. It is shown that including a priori knowledge o...
Verification and transformation of complex and uncertain conceptual schemas Yazıcı, Adnan (World Scientific Pub Co Pte Lt, 1997-12-01) In database environment it is necessary to represent complex and uncertain information at conceptual level and then transform the conceptual schema into the logical one for ultimate implementation. It is also important to verify the conceptual schema with respect to the constraints imposed on the schema definition. In this paper we primarily focus on the verification and transformation of the conceptual schema For the purpose of verification of the conceptual schema represented by the ExIFO data model (the ...
Implementation and simulation of mc68hc11 microcontroller unit using systemc for co-design studies Tuncalı, Cumhur Erkan; Aşkar, Murat; Department of Electrical and Electronics Engineering (2007) In this thesis, co-design and co-verification of a microcontroller hardware and software using SystemC is studied. For this purpose, an MC68HC11 microcontroller unit, a test bench that contains input and output modules for the verification of microcontroller unit are implemented using SystemC programming language and a visual simulation program is developed using C# programming language in Microsoft .NET platform. SystemC is a C++ class library that is used for co-designing hardware and software of a system...

Citation Formats

K. V. Schmidt, “Verification of Modular Diagnosability With Local Specifications for Discrete-Event Systems,” IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, pp. 1130–1140, 2013, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/34393.