University of Michigan, Ann Arbor
June 26-27, 2000
A demonstration of prototype software tools for the design, modeling, and simulation of manufacturing process control and automation systems, based on the IEC 61131-3 and 61499
The University of Michigan Discrete Event Systems group has developed a methodology for the diagnosis of certain classes of failures in engineering systems. This approach is set in the framework of formal languages and their associated state machine representations. It is centered on the property of diagnosability of discrete event systems. Failure diagnosis is implemented by means of a state machine called the diagnoser, which is built from the system model. Recently, we began addressing the problem of failure diagnosis in discrete event systems with decentralized information. We propose a coordinated decentralized architecture consisting of local sites communicating with a coordinator that is responsible for diagnosing the failures occurring in the system. We have designed protocols, i.e., the diagnostic information generated at the local sites, the communication rules used by the local sites, and the coordinator's decision rule, that realize the proposed architecture.
To design and analyze a logic controller there are basically two approaches, model-based and non-model-based. Model-based approaches can be further grouped into two types, synthesis and verification. The synthesis approach is the one most closely related to Control Theory. Here a model of the uncontrolled process is build and based on formal specifications a controller is derived mathematically. The verification approach takes a model of the uncontrolled process and a model of the controller. The combination of both results in a model of the controlled process. Using this combined model formal specifications can be verified mathematically. Non-model-based approaches stem from the area of Software Engineering. They measure or verify certain properties of a piece of software under minimal or no assumptions about its environment. This approach is well suited for logic controllers because of two main reasons. First of all, the realization of a logic controller includes hard- and software. But under the assumption of standard hardware with well-defined functionality, the application is realized by the program of the control algorithm, i.e. software. Hence the quality and functionality of the controller depends mainly on the quality and functionality of that software. Furthermore, a model of the process under control is in most cases not readily available. Non-model-based analysis methods for logic control algorithms based on Signal Interpreted Petri Nets (SIPN) are presented. They include correctness analysis (unambiguity, determinism, ...) and the measurement of transparency. A control algorithm is said to be transparent if it is easy and clear to see what the controller does in a given situation and what it will do in the next step. And if it is possible to reinterpret the algorithm (i.e. the aim of the algorithm is easily recognizable). Because of a close relation between SIPN and Sequential Function Chart (SFC) according to IEC61131-3 standard the SIPN can easily be implemented on programmable logic controllers.
Automated control synthesis methods for discrete-event systems promise to reduce the time required to develop, debug, and modify control software. Such methods must be able to translate high-level control goals into detailed sequences of actuation and sensing signals. In this session, we present such a technique and demonstrate its implementation as a set of software tools called "Spectool". The software relies on a description of the plant defined through a set of interacting component models, each represented as a form of condition system Petri net. Control logic modules, called taskblocks, are synthesized from these individual models. These then interact hierarchically and sequentially to drive the system through specified control goals. The resulting controller is automatically converted to C++ code which is compiled and executed.
In this poster, we present a hierarchical structure and framework for the modeling, specification, analysis and design of controllers for a Reconfigurable Machining System (RMS). This hierarchical framework allows one to integrate controllers at various levels of coordination in the manufacturing system. Our approach is modular and ``object oriented''. This allows re-usability and rapid reconfigurability of the controller as the manufacturing system is reconfigured. We utilize the concept of timed transition models (TTM) introduced by Ostroff to model an RMS. We present a CAD tool SF2STeP that allows us to model a TTM in Stateflow and verify the correctness of the Stateflow diagram (representing the TTM) in STeP. To specify the desired controlled behavior of the RMS, we use the tools of Real Time Temporal Language(RTTL) introduced by Manna and Pnueli. In this framework, the controller analysis problem can be posed as the problem of verifying that certain logical ! formulae are valid. Such verification can be carried out using either theorem proving techniques or model checking. We present some analytical results on a problem of system reconfiguration. An iterative approach for designing a controller based on the analysis result mentioned above is also presented. Using this approach, we can design a controller for a given set of closed loop properties which guarantees correctness of the closed loop system. It has been observed that the behavioral temporal properties can be proved without much difficulty, but proving explicit timing properties is not currently possible in this framework. It also illustrates how the state explosion problem inherent in model-checking can be handled effectively by performing modular verification.
A simple educational test-bed that simulates an automated car assembly line has been built using LEGO blocks, for studying the application of the supervisory control theory (SCT) in manufacturing systems. Finite automata are used for modeling the operations of the assembly line, and for the specifications that accomplish the task of successfully completing the assembly repeatedly. Using a set of desired safety and progress specifications for assembly, we use supervisory control techniques for automatically deriving a supervisor that enforces the specifications while offering the maximum flexibility of assembly. For implementation of the control, a controller is extracted out of the supervisor by selecting, when possible, only one controllable event from among the ones allowed by the supervisor.
The machining systems considered in this work are high volume transfer lines which are widely used in automotive manufacturing. In these machining systems, several machines are linked together to provide complete processing of a machined part. The logic controller for a machining system is a discrete event supervisory system. Generally, it has three control modes: auto, hand, and manual. This work addresses a formal representation of logic controllers with three control modes in modularized structures using Petri net formalism. By considering the fault recovery processes of operations, two operation modules are developed. The structure of the modular logic controller is introduced and its properties are verified using well-known theorems for state machines. Each station control module can be represented by connecting operation modules; their connection algorithms are provided. If the connection algorithms are followed, live, safe, and reversible Petri nets can be obtained. A condition for a modular logic controller to generate correct control logic is presented. The actual logic control program can be generated directly from the Petri net models by using IEC1131-3 programming languages. Moreover, the proposed modular Petri net structure can be used in control logic reconfiguration and automatic code generation.
The FSMGenerator is a software tool that enables direct manipulation of FSM control logic. Graphic representation can play an important role in understanding the overall structure and relations modeled by the FSM as well as providing a much faster and robust method of modification than direct coding (as most FSM logic is currently done). It can even import an existing text-based FSM to automatically create an aesthetically acceptable initial graphical layout. Through the use of different “export filters,” it is designed to be user-extensible, allowing for the automatic generation of custom source code. This makes it a useful tool for translation into the syntax of virtually any existing system that uses FSM logic, including third party verification tools. Alternatively, the FSMs generated through the program can be used directly in other Java programs designed to utilize it making file management much easier.
In this paper, we present an initial formulation of a logical approach to the synthesis of supervisory controllers for finite automata where the class of specified tasks to be realised by the automaton includes the newly defined LOOP-SPEC type of iterated tasks. The resulting version of the COCOLOG logic control system is called the S-COCOLOG system. Algorithmic procedures for the synthesis of S-COCOLOG Supervisory Conditional Control Rules (SCCRs) (when such SCCRs exist) for any given automaton and any given set of LOOP-SPECs are presented. The formulation, specification structures and algorithms developed in the automaton case above all have corresponding formulations in the finite state machine (FSM) case.
We consider a generalized form of the conventional decentralized control architecture for discrete-event systems where the control actions of a set of supervisors can be ``fused'' using both union and intersection of enabled events. Namely, the supervisors agree a priori on choosing ``fusion by union'' for certain controllable events and ``fusion by intersection'' for certain other controllable events. We show that under this generalized architecture, a larger class of languages can be achieved than before since a relaxed version of the notion of co-observability appears in the necessary and sufficient conditions for the existence of supervisors.