Open Access Unrestricted online access star

In recent decades, discrete-event modelling has been widely utilised to address control engineering problems. Comparing with conventional dynamic system modelling where physical behaviour is explicitly to describe, discrete-event modelling focuses on a more abstract level where logical behaviour is of interest. In this dissertation, we focus on the formal verification of the logical closedloop behaviour of control systems. To satisfy safety and/or liveness requirements according to given technical specifications, we exploit the formal semantics of control programmes to represent the entire closed-loop behaviour in a discrete-event model, from which the properties of interest can be formally verified through an efficient method.

Accessibility options of PDF file not available

Creative Commons Licence cc by cc https://creativecommons.org/licenses/by/4.0/

eng

Freely available e-book