|
AbstractIn this thesis we present a hierarchical method that decomposes a system into a high level subsystem which communicates with n >= 1 parallel low level subsystems through separate interfaces, which restrict the interaction of the subsystems. We first define the setting for the serial case (n = 1), and then generalise it for n >= 1. We present a definition for an interface, and define a set of interface consistency properties that can be used to verify if a discrete-event system (DES) is nonblocking and controllable. Each clause of the definition can be verified using a single subsystem; thus the complete system model never needs to be constructed, offering significant savings in computational effort. Additionally, the development of clean interfaces facilitates re-use of the component subsystems. We then provide a set of algorithms for evaluating these properties.Finally, we present the application of the method to a model of the Atelier Interetablissement de Productique (AIP), a large (7 x 10^21 possible states), highly automated, manufacturing system. |
Shift+click to download: leducPhd.ps.zip (4Mb compressed postscript. Use unzip, or pkunzip to uncompress), or leducPhd.pdf (6Mb PDF).