This thesis focuses on issues related to implementing theoretical Discrete-Event Systems (DES) supervisors, and the concurrency and timing delay issues involved. Sampled-data (SD) supervisory control deals with timed DES (TDES) systems where the supervisors will be implemented as SD controllers. An SD controller is driven by a periodic clock and sees the system as a series of inputs and outputs. On each clock edge (tick event), it samples its inputs, changes states, and updates its outputs. In this thesis, we identify a set of existing TDES properties that will be useful to our work, but not sufficient. We extend the TDES controllability definition to a new definition, SD controllability, which captures several new properties that will be useful in dealing with concurrency issues, as well as make it easier to translate a TDES supervisor into an SD controller. We then establish a formal representation of an SD controller as a Moore Finite State Machine (FSM), and describe how to translate a TDES supervisor to a FSM, as well as necessary properties to be able to do so. We discuss how to construct a single centralized controller, as well as a set of modular controllers and show that they will produce equivalent output. Next, we capture the enablement and forcing action of a translated controller in the form of a TDES supervisory control map, and show that the closed-loop behavior of this map and the plant is the same as that of the plant and the original TDES supervisor. We also show that our method is robust with respect to nonblocking and certain variations in the actual behavior of our physical system. We also introduce a set of predicate-based algorithms to verify the SD controllability property, as well as certain other conditions that we require. We have created a software tool for verifying these conditions and provide the source code in the appendix. We have implemented these algorithms using binary decision diagrams (BDD). For illustrative purpose, we have produced a set of examples which fail the key conditions discussed in this thesis, as well as a successful application example based on a Flexible Manufacturing System. We also presented the corresponding FSM, translated from the example's supervisors. / Thesis / Master of Applied Science (MASc)

<p>Sampled-data supervisory control deals with timed discrete event systems (TDES) where the supervisors are to be implemented as sampled-data controllers. A sampled-data controller views the system as a series of inputs and outputs and is controlled by a periodic clock. It samples its inputs, changes state, and updates its outputs on each clock edge (the tick event). The sampled-data supervisory control framework provides a set of conditions that the TDES system must satisfy to ensure its correct behaviour in order to be implemented as sampled data controllers. A serious limitation for automatic verification of systems is the size of the system's synchronous product. To overcome this limitation, we propose the use of a compositional approach to the verification of sampled-data supervisory control. In this approach, first we recast the required conditions for sampled-data supervisory control in terms of other properties such as language inclusion, nonblocking or controllability, which already have existing compositional methods and algorithms. This makes the sampled-data properties suitable for compositional verification, considerably increasing the size of systems that can be handled using sampled-data supervisory control. We also develop and implement a set of algorithms for the compositional verification of these sampled-data properties. We provide an example of the SD Controlled Flexible Manufacturing System to test our algorithms.</p> / Master of Science (MSc)

In the area of Discrete Event Systems (DES), formal verification techniques are important in examining a variety of system properties including controllability and nonblocking. Nonetheless, in reality, most software and hardware practitioners are not proficient in formal methods which holds them back from the formal representation and verification of their systems. Alternatively, it is a common observation that control engineers are typically familiar with Moore synchronous Finite State Machines (FSM) and use them to express their controllers’ behaviour. Taking this into consideration, we devise a generic and structured approach to automatically translate Moore synchronous FSM into timed DES (TDES) supervisors. In this thesis, we describe our FSM-TDES translation method, present a set of algorithms to realize the translation steps and rules, and demonstrate the application and correctness of our translation approach with the help of an example. In order to develop our automatic FSM-TDES translation approach, we exploit the structural similarity created by the sampled-data (SD) supervisory control theory between the two models. To build upon the SD framework, first we address a related issue of disabling the tick event in order to force an eligible prohibitable event in the SD framework. To do this, we introduce a new synchronization operator called the SD synchronous product (||SD), adapt the existing TDES and SD properties, and devise our ||SD setting. We formally verify the controllability and nonblocking properties of our ||SD setting by establishing logical equivalence between the existing SD setting and our ||SD setting. We present algorithms to implement our ||SD setting in the DES research tool, DESpot. The formulation of the ||SD operator provides twofold benefits. First, it simplifies the design logic of the TDES supervisors that are modelled in the SD framework. This results in improving the ease of manually designing SD controllable TDES supervisors, and reduced verification time of the closed-loop system. We demonstrate these benefits by applying our ||SD setting to an example system. Second, it bridges the gap between theoretical supervisors and physical controllers with respect to event forcing. This makes our FSM-TDES translation approach relatively uncomplicated. Our automatic FSM-TDES translation approach enables the designers to obtain a formal representation of their controllers without designing TDES supervisors by hand and without requiring formal methods expertise. Overall, this work should increase the adoption of the SD supervisory control theory in particular, and formal methods in general, in the industry by facilitating software and hardware practitioners in the formal representation and verification of their control systems. / Dissertation / Doctor of Philosophy (PhD)