Abstract

The Supervisory Control Theory (SCT) of Discrete Event Systems (DES) provides a framework for synthesizing a DES supervisor to ensure a DES plant satisfies its design specification. In SCT, supervisor synthesis is performed offline before the functioning of the plant. Generally, the size of the plant and the specifications models are large resulting in supervisors that need huge computer memory for storage -- usually unavailable in embedded systems. A solution to this problem proposed in the literature is Limited Lookahead Policy (LLP). In LLP, the supervisory control commands are calculated online during the plant operation. After the occurrence of each event, the next control command is calculated based on the plant behaviour over a limited number of events into the future. In practice such frequent LLP computation would not be feasible as multiple events can occur consecutively over a short duration, not leaving enough time for LLP computation between them. To tackle this issue, a method is proposed called LLP with Buffering where the supervisory control commands are calculated online and buffered in advance for a predefined window of events in future. Determining the correct size of the buffer is crucial in order to achieve a trade-off between the on-board memory requirement and the computational resources and also ensuring that new supervisor commands are computed before the buffer runs out empty. The size of the buffer primarily depends on (1) the execution time of the code for supervisor calculation and (2) the (fastest) rate of event generation in the plant. This thesis focuses on the second factor. Previously, the minimum execution duration of event sequences has been calculated experimentally. The experimental approach is not exhaustive and thus results in an overestimate in the value of the minimum execution duration of event sequences. In this thesis, a model-based approach to the computation of the minimum duration is proposed which begins by transforming the untimed model of the plant under supervision into a timed automaton (TA) by incorporating timing information of the events. Next, an exhaustive symbolic matrix-based search algorithm is proposed where all the event sequences from every mode of the TA model are traversed to determine the minimum execution duration of the event sequences. The proposed method avoids the reachability analysis of TA needed to determine the reachable clock regions for each mode. The number of these regions is exponential in the number of events. Instead, the method uses reachability on the graph of the untimed model (polynomial in the number of events). This algorithm runs faster but provides an underestimate for the minimum execution duration of event sequences. Next, a two-degree-of-freedom solar tracker system is used as a plant to analyse the timing behaviour of the events and the implementation of LLP with buffering. In this study, the model-based and experimental methods have been used together to choose a suitable buffer size. The resulting LLP supervisor with buffering has been successfully implemented.