A Compositional Approach for Verifying Sampled-Data Supervisory Control

Mahvash Baloch, M.Sc. Thesis, Dept. of Computing and Software, McMaster University, March 2012.


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.


Shift+click to download: mBalochMScThesis.pdf (760kB PDF).