Abstract The Eclipse Supervisory Control Engineering Toolkit (ESCET™) is an open-source project to provide a model-based approach and toolkit for developing supervisory controllers, targeting their entire engineering process. It supports synthesis-based engineering of supervisory controllers for discrete-event systems, combining model-based engineering with computer-aided design to automatically generate correct-by-construction controllers. At its heart is supervisory controller synthesis, a formal technique for the automatic derivation of supervisory controllers from the unrestricted system behavior and system requirements. Vital for the future development of these techniques and tools is the ESCET project’s open environment, allowing industry and academia to collaborate on creating an industrial-strength toolkit. We report on some crucial developments of the toolkit in the context of research projects with Rijkswaterstaat and ASML that have considerably improved its capability to deal with the complexity of real-life systems as well as its usability.

This paper discusses a method to distribute a synthesized supervisor for implementation on multiple physical controllers. Dependency structure matrices are used to determine a distribution of a system. The supervisor is then distributed accordingly, using an existing localization method. Communication delays between the distributed components of a supervisor may affect its behavior, due to changes in the order of events. Therefore, a new delay-robustness check is proposed and where needed mutex locks are employed to make the distributed supervisor delay robust. The controller performance is analyzed and optimized through a parameter study and a mutex implementation evaluation. In a real-life case study, the method is demonstrated by synthesizing, distributing, implementing, and validating a supervisor for a road tunnel.Note to Practitioners—This article is motivated by the desire to bridge the gap between the asynchronous, discrete-event, world of synthesized supervisors and the synchronous, real-time, world of networked PLC controllers. The main focus lies on maintaining the guarantees of supervisor synthesis while taking into account all aspects of real-time implementation, such as cycle-driven code execution and communication delays.

In case of malfunctions or accidents related to an infrastructural system, it is useful to reconstruct and analyze the behavior that led to such an undesired situation. Understanding the behavior can help in improving the plant and the supervisory controller such that this situation is not encountered again. Many computer-controller mechanical systems use programmable logic controllers (PLCs) to implement the supervisory controller and to collect data from the system. Currently, incident analysis for PLCs often consists of plotting actuator and sensor signals to reconstruct and analyze the behavior. This way of analyzing is laborious and difficult to interpret for engineers not familiar with the system. In this paper, a different behavioral reconstruction and analysis method is proposed. In this method, models developed during the design of the supervisory controller are reused. From the collected data, a finite-state automaton is constructed. This automaton can be used for behavioral reconstruction via simulation, which is simpler and more intuitive. Moreover, by comparing the logged behavior with the behavior defined in the available models, faults can be identified. As a proof of concept, the behavior of a real movable bridge has been logged from a PLC, reconstructed, simulated, and analyzed.

In this paper, we present a case-study on application of Ramadge-Wonham supervisory control theory (abbreviated by SCT in the sequel) to a patient support system of a magnetic resonance imaging (MRI) scanner. We discuss the whole developmental cycle, starting from the mathematical models of the uncontrolled system and of the control requirements, and ending with the implementation of the obtained controller on the actual hardware. The obtained controller was tested on the physical system. In this case study, we attempted to build the models in a modular way, in order to decrease the computational complexity of the controller synthesis and to improve the adaptability of the models. An important advantage of SCT is that it allows automatic generation of the controller, and that it can thus improve adaptability of the control software. We also briefly discuss our experience on the adaptability of the control software, obtained in the course of this case study.

The integration and test phase of complex manufacturing machines, like an ASML lithographic manufacturing system, is expensive and time consuming. The tests that can be performed at a certain point in time during the integration phase depend on the modules that are integrated and, therefore, on the preceding integration sequence. In this paper, we introduce a mathematical model to describe an overall integration and test sequencing problem, and we propose an algorithm to solve this problem. The method is a combination of integration sequencing and test sequencing. Furthermore, we introduce several strategies that determine when test phases should start. With a case study within the development of a software release that is used to control an ASML lithographic machine, we show that the described method and strategies can be used to solve real-life problems.

Testing complex systems, such as the ASML TWINSCAN lithographic machine, is expensive and time consuming. In a previous work, a test sequencing method to calculate time-optimal test sequences has been developed. Because complex systems are composed of several subsystems, which are again composed of several modules, there exists a need to hierarchically model test sequencing problems. Such a hierarchical test sequencing problem consists of a high-level model that describes a test sequencing problem at the system level, and one or more low-level models that describe the test sequencing problems at the subsystem or module level. The tests at the system level correspond to the solutions of low-level problems. This paper describes a hierarchical test sequencing model and proposes two algorithms to compute an optimal test sequence. The benefits of hierarchically modeling a problem are less computational effort and less modeling effort, because not all relations are needed. This is illustrated by a small example. The industrial relevance of this method is illustrated on a case study related to a manufacturing testing phase of a lithographic machine.

Testing complex manufacturing systems, such as an ASML lithographic machine, takes up to 45% of the total development time of a system. The problem of which tests must be executed in what sequence to ensure in the shortest possible test time that the system works, which is the test-sequencing problem, was already solved by Pattipati et al. for the diagnosis of systems during operation. Test-sequencing problems during the development and manufacturing phases of systems, however, require a different approach than the test-sequencing problems during operation. In this paper, the test problem description and algorithms developed by Pattipati et al. are extended to solve test-sequencing problems for the development and manufacturing of manufacturing systems. For a case study in the manufacturing process of an ASML lithographic machine, it is shown that solving a test-sequencing problem with this method can reduce the test time by 15% to 30% compared to experts that solve this problem manually.

Testing complex manufacturing systems, like ASML lithographic machines, can take up to 45% of the total development time. The decision of when to stop testing is often difficult to make because less testing may leave critical faults in the system, while more testing increases time-to-market. In this paper, we solve the problem of deciding when to stop testing by introducing a test-sequencing method that incorporates several stopping criteria. These stopping criteria consist of objectives and constraints on the test cost and the remaining risk cost. For a given problem, a suitable stopping criterion can be chosen. For example, with the risk-based stopping criterion, testing stops when the test time or cost exceeds the risk cost. Furthermore, we show that it also is possible to model reliability problems with this test-sequencing method. The method is demonstrated on ASML systems with two case studies. The first case study was conducted in the test phase during the development of the software that is used to control an ASML lithographic machine. The second case study was conducted on the reliability testing of a lithographic machine.

Studying industrial systems by simulation enables the designer to study the dynamic behaviour and to determine some characteristics of the system. Unfortunately simulation also has some disadvantages. These can be overcome by using formal methods. Formal methods allow a thorough analysis of the possible behaviours of a system, parameterised system analysis and a modular approach to the analysis of systems. We present a case study in which a model of an industrial system is studied in a formal way. For this purpose, the model is first specified and simulated using the CSP-based executable specification language /spl chi/. The model is translated into a model in the process algebra ACP/sup T/. This enables us to give a correctness proof of the parameterised model and to study the model in isolation.