Closed-Loop Formal Verification Framework with Non-determinism, Configurable by Meta-modelling

被引：0

作者：

Patil, Sandeep ^{[1
]}

Bhadra, Sayantan ^{[1
]}

Vyatkin, Valeriy ^{[1
]}

机构：

[1] Univ Auckland, Ctr Sci, Auckland 1, New Zealand

来源：

IECON 2011: 37TH ANNUAL CONFERENCE ON IEEE INDUSTRIAL ELECTRONICS SOCIETY | 2011年

关键词：

Model-checking; NCES; meta-modelling; industrial automation; formal verification; simulation; SYSTEMS;

D O I：

暂无

中图分类号：

T [工业技术];

学科分类号：

08 ;

摘要：

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.

引用

页码：3770 / 3775

页数：6

共 3 条

[1] Semi-formal verification of closed-loop specifications in the concept design phase
Richter, Jan H.
Friedrich, Stefan R.
AT-AUTOMATISIERUNGSTECHNIK, 2017, 65 (02) : 115 - 123
[2] Neural networks in closed-loop systems: Verification using interval arithmetic and formal prover
Rossi, Federico
Bernardeschi, Cinzia
Cococcioni, Marco
ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE, 2024, 137
[3] A flux pump driven non-soldering closed-loop HTS magnet and its electromagnetic-thermal semi-analytical modelling method
Zhu, Lingfeng
Wang, Yinshun
Gao, Hanzhi
Hu, Chengyang
Liu, Wei
Wang, Jiawen
Sun, Yudong
SUPERCONDUCTOR SCIENCE & TECHNOLOGY, 2024, 37 (01)

← 1 →