This work proposes a novel approach for controller synthesis on the shop-floor level for discrete-event systems. The approach is based on a modular modeling formalism and structural properties of models of uncontrolled plant behavior that are designed using this modeling formalism. The approach takes advantage of the transition invariants of the underlying Petri net components of the model and uses the event interconnections of transitions that are part of the transition invariants. The result is the so-called transition invariant graph that represents a new structural property of the modeled system. The synthesis procedure takes models of the uncontrolled plant behavior and formal specifications of the desired cyclic plant behavior under control and forbidden states as well. From these ingredients, the transition invariant graph is computed from which the admissible trajectories are extracted. This is performed by partial reachability analysis. An example taken from a lab-scaled manufacturing system illustrates the methodology and shows the application. The complexity of the synthesis procedure is significantly reduced. That makes it feasible to be used for even larger systems of real industrial scale.

In each of Fig. 1(a), (c), (e), and (f) in the above-named article [ibid., vol. 42, no. 1, pp. 178-191, Jan. 2012], there is an arc from transition t3 to place p6, which is incorrect. The arc between the transition and the place should be from p6 to t3. The Petri net depicted in Fig. 1(a) is a well-known example that has been widely utilized in the literature.

Control software engineering has become a weighty factor according to implementation expense, especially when developing a new plant or migrating an existing one. Because of this, there are high customer demands concerning safety and correctness of software. Conventional open-loop testing methods have clearly reached their limits as the complexity of today's control software is not manually manageable anymore. Nevertheless, they still belong to daily practice due to the lack of integrated solutions that do not overcharge users but that are tailored to software engineering demands. This contribution ther-fore approaches this problem and encourages the application of closed-loop modeling, validation, and verification methods. Beyond this, it proposes complete frameworks to apply this expertise not only in academia but in industrial environment as well.

Deadlocks are an undesirable situation in automated flexible manufacturing systems (FMS). Their occurrences often deteriorate the utilization of resources and may lead to catastrophic results. Finding an optimal supervisor is NP-hard. A computationally efficient method often ends up with a suboptimal one. This paper develops a deadlock prevention method that makes a good tradeoff between optimality and computational tractability for a class of Petri nets, which can model many FMS. The theory of regions guides our efforts toward the development of near-optimal solutions for deadlock prevention. Given a plant net, a minimal initial marking is first decided by structural analysis, and an optimal live controlled system is computed. Then, a set of inequality constraints is derived with respect to the markings of monitors and the places in the model such that no siphon can be insufficiently marked. A method is proposed to identify the redundancy condition for constraints. For a new initial marking of the plant net, a deadlock-free controlled system can be obtained by regulating the markings of the monitors such that the inequality constraints are satisfied, without changing the structure of the controlled system. The near-optimal performance of a controlled net system via the proposed method is shown through several examples.

The paper deals with reconfigurable embedded control systems following different component-based technologies and/or Architecture Description Languages used today in industry. We define a Control Component as a software unit to support control tasks of the system, which is assumed to be a network of components with precedence constraints. We define an agent-based architecture to handle automatic reconfigurations under well-defined conditions by creating, deleting, or updating components to bring the whole system into safe and optimal behaviors. To cover all possible reconfiguration forms, we model the agent by nested state machines according to the formalism Net Condition/Event Systems (NCESs), which is an extension of Petri nets. In addition, we apply a model checking to verify functional and extra-functional properties according to the temporal logic "Computation Tree Logic” (CTL). The goal is to check the agent reactivity after any evolution of the environment. Several complex networks can implement the system, where each one is executed at a given time when a corresponding reconfiguration scenario is automatically applied by the agent. To check the correctness of each one of them, we apply in several steps a refinement-based approach that automatically specifies feasible Control Components according to NCES. The model checker SESA is automatically applied in each step to verify deadlock properties of new generated components, and it is manually used to verify CTL-based properties according to user requirements. We implement the reconfiguration agent by three modules that allow interpretations of environment evolutions, decisions of useful reconfiguration scenarios, and finally, their applications. Two Industrial Benchmark Production Systems FESTO and EnAS available in our research laboratory are applied to explain the contributions of the paper.

This paper deals with distributed multi-agent reconfigurable embedded control systems following the International Industrial Standard IEC 61499 in which a Function Block (FB) is an event-triggered software component owning data and a control application is a network of distributed blocks that should satisfy functional and temporal properties according to user requirements. We define an architecture of reconfigurable multi-agent systems in which a Reconfiguration Agent is affected to each device of the execution environment to apply local reconfigurations, and a Coordination Agent is proposed for coordinations between devices in order to guarantee safe and adequate distributed reconfigurations. A communication protocol is proposed to handle coordinations between agents by using well-defined Coordination Matrices. We specify both reconfiguration agents to be modeled by nested state machines, and the Coordination Agent according to the formalism Net Condition-Event Systems (NCES) which is an extension of Petri nets. To validate the whole architecture, we check by applying the model checker SESA in each device functional and temporal properties to be described according to the temporal logic “Computation Tree Logic.” We have also to check all possible coordinations between devices by verifying that whenever a reconfiguration is applied in a device, the Coordination Agent and other concerned devices react as described in user requirements. The paper's contributions are applied to two Benchmark Production Systems available in our research laboratory.

This paper addresses a component-based approach using the Event-B method to develop automated systems. These systems are composed of two parts: the control part (controller) and the operative part (controlled component). The first is a software component which controls the operative part that models the physical device and its environment. We propose in this paper the use of the formal Event-B method to develop automated systems applying a codesign technique, where the two components are developed separately, and then, a composition is defined with the Event-B method to prove the automated system correctness. First of all, we define a specification for the composition of these two components in the Event-B method. Second, we give refinement semantics for a component-based system before proposing a method to verify the refinement of a whole system from that of its components.

Programmable Logic Controllers (PLCs) have been established as standard devices for automation and process control since the 1990s. Although a lot of research work has been done on the field of controller modeling and verification, it is still daily practice that control software is manually developed without applying formal validation methods. On the other hand, controller modeling is often seen detached from the plant or its model, i.e. as an open loop. The results of analysis of open-loop controller behavior give very little or almost no indications of the correct behavior of the closed-loop system. The contribution therefore proposes an approach to generate formal models out of PLC code. These controller models enable formal verification of the closed loop in combination with a specification. Due to the year of publication, all solution approaches are based on the syntax definition of the IEC 61131-3, which is not fulfilled by every industrial PLC vendor. Therefore, this contribution will show a way to use the defined xml formats of the Technical Committee 6 of the PLCopen as input for the formal model generation.

It was shown in former publications that, in principle, the design of a distributed control system according to IEC 61499 could be proven to be correct. An implementation of such a control system should run correctly. But there are known issues regarding the specification and implementation of IEC 61499 function blocks execution models, which cause a verified control system design does not necessarily resulting in an implementation with the desired behavior. Another issue influencing the verification process is the granularity of the formal models used for verification. Bringing more plant properties (i.e. time related) into formal models for closed-loop verification will improve the verification process and reliability in its result. In this contribution the authors want to draft a way of covering the above-mentioned issues using the known Net Condition/Event Systems (NCES) as formal models.

This paper1deals with the model checking of Safe Heterogeneous Embedded Control Systems following different component-based technologies or implemented according to different Architecture Description Languages (ADL) used today in industry. The purpose is to reduce their time to market by exploiting various execution environments and different rich libraries. A ¿Control Component¿ is defined in our research work as an event-triggered software unit composed of an interface for any external interactions and an implementation allowing control actions of physical processes. A control system is assumed to be a composition of components with precedence constraints to control the plant according to well-defined execution orders. We define an agent-based architecture where the agent controls the environment evolution and applies automatic reconfigurations when hardware errors occur at run-time to guarantee a functional safety of the whole system. We model the architecture according to the formalism Net Condition/Event Systems (abbr. NCES), and apply the model checker SESA to check functional properties described according to the well-known Computation Tree Logic (abbr. CTL). Our purpose is to check that whenever an error occurs at run-time, the agent behaves as described in user requirements by activating Control Components and deactivating others to guarantee a functional safety of the whole system. A Benchmark Production System is used in this research work to explain our contribution.

The paper deals with the implementation of reconfigurable embedded control systems following the Component-based International Industrial Standard IEC61499, in which a Function Block is an event triggered software component owning data and an application is a composition of blocks. To handle automatic reconfigurations of the whole system, we define an agent-based architecture such that the agent checks and interprets the environment evolution before creates, updates or deletes Function Blocks according to well-defined conditions. It is composed of three modules: the interpreter that interprets the environment evolution, the engine that decides new reconfigurations according to such evolution and the converter that applies agent decisions. A Benchmark Production System is used to explain our contribution, and technical solutions are proposed to implement its different agent modules.

Manual reconfiguration of existing systems is a common task for engineers. Especially, the modernization of plants depends on an unambiguous and reliable documentation. Furthermore, the well-defined specification of plant behavior enables the engineer to verify the control software with a model-checking tool. In order to be able to provide the description correctly and without misunderstandings, it should be done formally. Temporal logics, like the Computation Tree Logic, offer an ideal solution for this purpose. However, they are based on a complex theory. In order to use them anyway in practice, the formal expressions have to be developed by automated procedures out of an intuitively understandable description. This contribution proposes a text-block based method, which enables the user to create such a formal specification by the use of a Safety-Oriented Technical Language.

This paper presents a new framework for design and validation of industrial automation systems based on systematic application of formal methods. The engineering methodology proposed in this paper is based on the component design of automated manufacturing systems from intelligent mechatronic components. Foundations of such componentspsila information infrastructure are the new IEC 61499 architecture and the automation object concept. It is illustrated in this paper how these architectures, in conjunction with other advanced technologies, such as Unified Modeling Language, Simulink, and net condition/event systems, form a framework that enables pick-and-place design, simulation, formal verification, and deployment with the support of a suite of software tools. The key feature of the framework is the inherent support of formal validation techniques achieved on account of automated transformation among different system models. The paper appeals to developers of automation systems and automation software tools via showing the pathway to improve the system development practices by combining several design and validation methodologies and technologies.

This paper deals with automatic refinement-based specifications of feasible Control Tasks in Embedded Control Systems. By considering the Plant architecture, we model at first time the system with an abstract model according to the Net Condition Event System formalism and we automatically refine thereafter this model in different steps to define and specify Control Tasks that have to be checked in each step. This approach optimizes the development cost of complex Embedded Systems and it is applied on two Benchmark Production Systems FESTO and EnAS available in our research laboratory to prove its benefits.

This paper deals with the development of reconfigurable control systems following the component-based International Industrial Standard IEC61499. In this standard, a function block is an event-triggered component owning data and an application is a FB network that has to satisfy temporal properties. This network is totally changed or modified if a reconfiguration scenario is applied at run-time. We classify at first time all possible reconfiguration forms and we propose thereafter an Agent-based architecture to handle them. To verify temporal properties on the FB network corresponding to each reconfiguration scenario, we analyze the schedulability of the corresponding blocks. If it is feasible, then a static scheduling is generated as a sequencing to be used by the OS when the Agent applies at run-time the corresponding scenario. We deduce finally the whole system feasibility if the FB network corresponding to each possible scenario is feasible. A tool X - Reconfig is developed in our research laboratory to support the paper contribution.

Design and verification of distributed controllers according to the IEC 61499 standard are major issues for automation industry today. In this paper we introduce an enhanced development of the hierarchical control approach by means of a multi-layered architecture including distributed master controllers as a layered composition. A main focus in that control design is the high reusability of the controllers. We further address formal approaches to verify this control architecture in a hierarchical way as well. Therefore, we use the previously introduced methods of automation objects, which are a subject of work for many research groups nowadays.

This contribution deals with modelling of the uncontrolled plant behaviour on the sensor/actuator level that will eventually provide the basis for synthesis of distributed controllers. It presents a modular modelling formalism as well as a modelling methodology for model engineering rather than designing a model from scratch. The improved modelling formalism includes new modular system semantics. This enables us to study the dynamic behaviour of the modular model without performing a complete composition and thereby destroying the modular nature of the model. A well-structured modelling example of a laboratory plant is provided to illustrate the method. It shows that the method is able to cope with rather large systems of realistic scale.

This paper presents a new approach to modelling and verification of function block applications of the IEC 61499 standard. The approach uses the language of logic programming Prolog to represent a model of function block network and to verify its properties. The class of properties that can be checked is extended to more substantial queries providing in return not only "yes" or "no", but also the parameters explaining the reasons. The models essentially use the topological properties of the function block network and allow data of arbitrary types (not only Boolean) be used in the queries.

This contribution presents an approach for synthesis of distributed logic controllers based on modular plant models and forbidden states. Modular plant models are defined that keep the state distributed. Forbidden states are formulated by means of predicates. A backward search algorithm is applied to determine a monolithic controller for the specification. Afterwards, the controller is split into a network of communicating local controllers each imposing control on a part of the plant. It is proven that the network of local controllers realizes the same behaviour at the plant as the monolithic controller. An example illustrates the methodology.

This paper discusses systematic approaches to the design of distributed controllers in industrial automation systems. Several design approaches are compared that lead to the distributed control of manufacturing machines and their parts. In particular, a decentralized control method is introduced that does not require a master controller. The implementation frameworks of IEC 61131-3 and IEC 61499 are checked on their fitness to the distributed control. A migration method from a PLC-based control to IEC 61499 is illustrated. A layered architecture for distributed controllers is introduced and tested on examples.

The use of model-based code-generators for construction of controller software increases the reliability of the software in two ways: first, the models often can be checked for safety conditions. Second the use of code-generators prevents manual implementation faults. However, the reliability depends on the correctness of these code-generators, i.e., whether they really generate code that correctly implements the model. In this paper, we show how this correctness can be checked automatically for code-generators for PLCs.

This paper describes formal modeling and verification of automation systems from the system engineering point of view. Reuse of model components is the key issue in order to bring the scientific modeling methodology into engineering practice. The reuse is achieved by the combination of modular modeling of automation systems with object-oriented description of models in UML style. This allows to benefit from advantages of both worlds: efficiently manage highly hierarchical complex models with UML tools and end up with efficiently executable models with distributed states that are compatible also with IEC61499 function block specifications. The approach is supported by the tool framework that is described in the contribution

We describe here how to obtain a model for the admissible behavior of a Discrete Event System that is represented by a safe Petri Net model. The events of this Petri Net model may be controllable or uncontrollable. Also given is a sequential specification which is modeled with a special state machine. Then, using the condition and event arcs of Net ConditionlEvent Systems, a combined model of plant and specification is obtained. We use only the structure of this combined model to develop a method which gives the admissible behavior of the system. Thus, we avoid the complexity of a complete state enumeration.

We describe here how to obtain a model for the admissible behavior of a discrete event system that is represented by a safe Petri net (PN) model. The transitions of this PN model may be controllable or uncontrollable. Also given is a sequential specification which is modeled with a special state machine. Then, using the condition and event arcs of net condition/event systems, a combined model of plant and specification is obtained. We use only the structure of this combined model to develop a method which gives the admissible behavior of the system. Thus, we avoid the complexity of a complete state enumeration.

The demands of users and markets require today's manufacturing systems to be agile and flexible. Hence, the corresponding control systems need to be adaptable, reusable and re-configurable. This motivates development of the control architectures based on the concept of software components. The international standard IEC 61499 provides a function block architecture for industrial process measurement and control systems. According to this standard, a distributed control system can be structured by means of interconnection of software components. With the help of a prototype control system, this paper describes how to design a distributed control system based on the engineering methodologies of extended model/view/controller (MVC) and layered architecture MVC according to IEC 61499. The corresponding configurations for practical application are presented, including some methods to decompose the functionality of a distributed system into several components. The integration of visualization components is discussed in detail. This paper serves as an example on how to apply the IEC 61499 standard into practice.

Models of plant behavior are required to use formal methods of manufacturing execution systems (MES) application development. We present a manufacturing oriented modular approach for designing such models. The approach is a first step towards a predictive simulation system for operator support in control of complex, hybrid manufacturing systems in the plastics industry.

We propose an approach for integration of different levels of logistics and control in a uniform methodology. The main issue is that the formalisms we use on different levels allow fast and easy re-configuration at all levels, from business level down to shop floor control. The proposed technology promotes the plug & play concept and utilizes a similar formalism across all layers of an enterprise and between enterprises within a supply chain. Each plug & play component has embedded in it a controller which can be re-configured dynamically and automatically according to the rules and protocols defined at the upper layers of enterprise or the network it belongs to. Each component also embeds a monitoring system, which provides feedback on its status and if necessary can participate in a distributed diagnosis in the case of faults, drifts, and other disturbances. The paper presents the concepts we have been developing so far and addresses future work on integration of our approaches.

The paper presents a preliminary report on modeling parts of a modular production system, their dedicated controllers, and the appropriate methods of fault treatment on the level of net condition/event systems (NCES). To achieve practicability, NCES support a systematic and modular way of modeling more complex systems as well as concurrent and non-deterministic behavior which is highly beneficial for modeling and control of DES in failure situations as studies of existing methods show.

This paper discusses the issues related to the correctness of agile manufacturing systems with distributed architectures. The corresponding development of software engineering methods targets the goal of easy-reconfigurable, self-organized software similar to that of the hardware. However, existing methods of software validation (manual testing or computer-aided simulation) are too slow to keep up with the pace of reconfigurations. In this paper we present an approach and a software tools to incorporate the formal verification to the practice of control engineering. The software package "verification environment for distributed applications" (VEDA) has been developed for model-based simulation and verification with a homogeneous graphical user interface. Net condition event systems are used for the modeling. VEDA deals with distributed controllers as defined in IEC 61499 and automatically generates the formal model of the controller with the given source code.

In a search for an appropriate visual specification language to be applied in control engineering the timing diagram specification language is suggested. It is applied to the verification of distributed controllers following the standard IEC 61499. Specification of inputs and outputs of the controller are given in the graphical form of signal diagrams. The inputs are then converted into finite-state models, while the diagram of outputs is used to build equivalent analytic expressions in extended CTL. These two parts are used in formal verification of the control system.

We address the problem of obtaining a model for the admissible behavior of a discrete event system in the presence of uncontrollable events. We start with a safe Petri net model of the plant and a sequential specification modeled with a special state machine. Then, a combined model of plant and specification is obtained by using the condition and event arcs of net condition/event systems. Using the structure of this combined model, we are able to develop a method to obtain the admissible behavior which avoids the complexity of a complete state enumeration.

Petri nets have a longstanding history in controller design and implementation, and it is often told that they have the dominating position in this field due to the close relationship between Petri nets and Graphcet or other sequential function diagrams. We want to show that there are some severe problems when Petri nets are used to describe both: the controller and the plant under control. The nature of these problems is the lack of a concept of input and output signals and, moreover, the lack of a formal concept to interconnect systems modeled by Petri nets via signals. Although this is often neglected, it turns out to be a key issue if a model of the closed-loop behavior must be established as a precondition for formal controller verification. We present a signal extension for Petri nets and means for interconnecting an arbitrary number of those extended Petri nets. We come up with the conclusion that the resulting models are suited for controller verification. Although the graphical appearance shows similarities to Petri nets, the resulting models are no longer Petri nets.

In this paper, arc-timed Petri nets are used to model controlled real-time discrete event systems, and the control synthesis problem that designs a controller for a system to satisfy its given closed-loop behavior specification is addressed. For the problem with the closed-loop behavior specified by a state predicate, real-time control-invariant predicates are introduced, and a fixpoint algorithm to compute the unique extremal control-invariant subpredicate of a given predicate, key to the control synthesis, is presented. For the problem with the behavior specified by a labeled arc-timed Petri net, it is shown that the control synthesis problem can be transformed into one that synthesizes a controller for an induced arc-timed Petri net with a state predicate specification. The problem can then be solved by using the fixpoint algorithm as well. The algorithm involves conjunction and disjunction operations of polyhedral sets and can be algorithmically implemented, making automatic synthesis of controllers for real-time discrete event systems possible.

BatchMon is a model-based monitoring and decision support system for short-term resource allocation in recipe-controlled batch processes. The paper presents the further development of BatchMon which has been triggered by a prototype installation of BatchMon at a laboratory plant of a chemical company.

Models of uncontrolled plant behavior are required to use formal methods of logical controller synthesis. We present a modular, hierarchical, efficient technique for designing such models. Notions of controllability and observability are given, and some related synthesis problems are stated.

Timestamp Petri nets, introduced in this paper, offer a new method to deal with time critical problems in the field of automation of manufacturing systems. To each token in a timestamp net a timestamp is assigned, which denotes the time when the token was put on its place. In those nets intervals are assigned to the incoming edges of transitions, which describe the permeability of the edge relative to the token on the adjacent place. In timestamp nets it is possible that synchronizing transitions are not able to fire although they are supplied with tokens sufficiently, because their incoming edges are not permeable simultaneously. In this case we say the transition got timewise stuck. In this paper it is examined how transitions of a timestamp net are getting timewise stuck. Based on a symbolic analysis, these investigations can be reduced to solving systems of linear inequalities. The method can also be used to determine parameters for a timestamp net in order to prevent transitions from getting timewise stuck. We show the method's applicability by the dynamic model of a small technical plant as an example. Forbidden states of the uncontrolled system are described by transitions which can get timewise stuck. We use the method to determine time parameters of a controller, which ensures that forbidden states in the controlled system are unreachable.