Closed-loop formal verification framework with non-determinism, configurable by meta-modelling

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 verificati...

Full description

Saved in:
Bibliographic Details
Main Authors: Patil, S., Bhadra, S., Vyatkin, V.
Format: Conference Proceeding
Language:English
Subjects:
Aerospace electronics
Automata
Computational modeling
Control systems
Dependable Communication and Computation Systems
Explosions
Formal verification
industrial automation
Kommunikations- och beräkningssystem
meta-modelling
Model-checking
NCES
Sensors
simulation
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1553-572X
DOI:10.1109/IECON.2011.6119923