VERIFICATION OF EMBEDDED SUPERVISORY CONTROLLERS CONSIDERING HYBRID PLANT DYNAMICS
Sebastian Engell, Sven Lohmann, Olaf Stursberg · International Journal of Software Engineering and Knowledge Engineering · 2005
This contribution proposes a link between the specification of supervisory controllers by Sequential Function Charts (SFC) and the verification of embedded systems with hybrid dynamics. The SFC are transformed into modular timed automata using a procedure based on graph grammars. The resulting controller model is composed with a hybrid automaton (with possibly nonlinear continuous dynamics) that models the plant behavior. In order to verify safety properties of the composed system algorithmically, a tool implementing the recently proposed approach of counterexample guided model checking is employed. The procedure is illustrated for a processing system example.