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

fYear

2011

fDate

7-10 Nov. 2011

Firstpage

3770

Lastpage

3775

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;

fLanguage

English

Publisher

ieee

Conference_Titel

IECON 2011 - 37th Annual Conference on IEEE Industrial Electronics Society

Conference_Location

Melbourne, VIC

ISSN

1553-572X

Print_ISBN

978-1-61284-969-0

Type

conf

DOI

10.1109/IECON.2011.6119923

Filename

6119923