Verification of logic controllers for continuous plants using timed condition event-system models

被引：29

作者：

Kowalewski, S ^{[1
]}

Engell, S ^{[1
]}

Preussig, J ^{[1
]}

Stursberg, O ^{[1
]}

机构：

[1] Univ Dortmund, Dept Chem Engn, Proc Control Lab, D-44221 Dortmund, Germany

来源：

AUTOMATICA | 1999年 / 35卷 / 03期

关键词：

formal verification; programmable logic controllers; distributed control systems; discretization of continuous systems; hybrid systems; condition/event systems; timed automata;

D O I：

10.1016/S0005-1098(98)00179-4

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

An approach to the formal verification of logic controllers for processes with switched continuous dynamics is presented. The method builds on modular, timed discrete event models of the plant and the controller. Subsystems with continuous dynamics are approximated algorithmically. The formal verification consists of determining the reachable discrete states of the resulting model and comparing it to a set of undesired states. For this purpose, the tool HyTech is applied. The approach is illustrated by the treatment of a process engineering example. (C) 1999 Elsevier Science Ltd. All rights reserved.

引用

页码：505 / 518

页数：14

共 29 条

[1] A THEORY OF TIMED AUTOMATA [J].

ALUR, R ;

DILL, DL .

THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235

[2] SYMBOLIC MODEL CHECKING - 1020 STATES AND BEYOND [J].

BURCH, JR ;

CLARKE, EM ;

MCMILLAN, KL ;

DILL, DL ;

HWANG, LJ .

INFORMATION AND COMPUTATION, 1992, 98 (02) :142-170

[3] Computer-aided verification [J].

Clarke, EM ;

Kurshan, RP .

IEEE SPECTRUM, 1996, 33 (06) :61-67

[4]

David R., 1992, Petri Nets and Grafcet

[5] Modeling and safety verification of discrete/continuous processing systems [J].

Dimitriadis, VD ;

Shah, N ;

Pantelides, CC .

AICHE JOURNAL, 1997, 43 (04) :1041-1059

[6]

DIMITRIADIS VD, 1996, COMPUT CHEM ENG SS, V20, P503

[7]

Engell S, 1996, IEEE DECIS CONTR P, P142, DOI 10.1109/CDC.1996.574274

[8]

Engell S, 1995, EUROSIM '95 SIMULATION CONGRESS, P421

[9]

ENGELL S, 1996, AICHE S SERIES, V93, P165

[10]

*FDA, 1975, CURR GOOD MAN PRACT

← 1 2 3 →