Title :
Closed-loop formal verification framework with non-determinism, configurable by meta-modelling
Author :
Patil, Sandeep ; Bhadra, Sayantan ; Vyatkin, Valeriy
Author_Institution :
Sci. Centre, Univ. of Auckland, Auckland, New Zealand
Abstract :
Formal verification of embedded control systems using closed-loop plant-controller models is getting increasingly popular. In this paper we propose a new method reducing complexity of model-checking on account of infusing non-determinism into certain parts of the plant model during formal verification process guided by a software tool. Net Condition/Event Systems (NCES) formalism is used for modular design of closed-loop models which are verified by ViVe and SESA model-checkers. Its performance is compared to modelling with finite state verified with SMV and UPPAAL and is proven to be superior.
Keywords :
closed loop systems; computational complexity; control engineering computing; embedded systems; factory automation; finite state machines; formal verification; software tools; SESA model checker; ViVe model checker; closed loop formal verification process; closed loop plant controller model; embedded control system; meta modelling; modular design; net condition-event system formalism; software tool; Aerospace electronics; Automata; Computational modeling; Control systems; Explosions; Formal verification; Sensors; Model-checking; NCES; formal verification; industrial automation; meta-modelling; simulation;
Conference_Titel :
IECON 2011 - 37th Annual Conference on IEEE Industrial Electronics Society
Conference_Location :
Melbourne, VIC
Print_ISBN :
978-1-61284-969-0
DOI :
10.1109/IECON.2011.6119923
