Summary: | This thesis presents a formal method for the the design of optimal and provably correct procedural controllers for chemical processes modelled as Stochastic Discrete Event Systems (SDESs). The thesis extends previous work on Procedural Control Theory (PCT) [1], which used formal techniques for the design of automation Discrete Event Systems (DESs). Many dynamic processes for example, batch operations and the start-up and shut down of continuous plants, can be modelled as DESs. Controllers for these systems are typically of the sequential type. Most prior work on characterizing the behaviour of DESs has been restricted to deterministic systems. However, DESs consisting of concurrent interacting processes present a broad spectrum of uncertainty such as uncertainty in the occurrence of events. The formalism of weighted probabilistic Finite State Machine (wp-FSM) is introduced for modelling SDESs and pre-de ned failure models are embedded in wp-FSM to describe and control the abnormal behaviour of systems. The thesis presents e cient algorithms and procedures for synthesising optimal procedural controllers for such SDESs. The synthesised optimal controllers for such stochastic systems will take into consideration probabilities of events occurrence, operation costs and failure costs of events in making optimal choices in the design of control sequences. The controllers will force the system from an initial state to one or more goal states with an optimal expected cost and when feasible drive the system from any state reached after a failure to goal states. On the practical side, recognising the importance of the needs of the target end user, the design of a suitable software implementation is completed. The potential of both the approach and the supporting software are demonstrated by two industry case studies. Furthermore, the simulation environment gPROMS was used to test whether the operating speci cations thus designed were met in a combined discrete/continuous environment.
|