Verification of logic controllers for continuous plants using timed condition/event-system models (Q1301427)

A mathematically rigorous procedure is proposed for the verification of a logic controller, already designed in accordance with the specifications formulated for the exploitation of a given continuous-time process. The research is motivated by the lack of a systematic approach to logic controller design for technical systems comprising plans with continuous dynamics. Formal verification is built on modular, timed discrete event models of the plant and the controller. Subsystems with continuous dynamics are mapped to timed condition/event systems by an automatic abstraction procedure. The resulting models for the plant and the controller are composed so as to allow comparing the reachability discrete states of the overall model with a set of forbidden states derived from specifications. The computational complexity of this analysis requires adequate software tools (such as HyTech, used by the authors). A batch evaporation process is chosen as an illustrative example, placing emphasis on the appropriate reaction of the controller to a cooling breakdown of the condenser.