Using model-checking for Timed Automata to parameterize logic control programs

被引：1

作者：

Kowalewski, S ^{[1
]}

Engell, S ^{[1
]}

Huuck, R ^{[1
]}

Lakhnech, Y ^{[1
]}

Lukoschus, B ^{[1
]}

Urbina, L ^{[1
]}

机构：

[1] Univ Dortmund, Dept Chem Engn, Process Control Grp, D-44221 Dortmund, Germany

来源：

COMPUTERS & CHEMICAL ENGINEERING | 1998年 / 22卷

关键词：

Programmable Logic-Controllers; process safety; validation; Timed Automata; HyTech;

D O I：

10.1016/S0098-1354(98)00170-7

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

In this contribution we describe how the modeling and analysis framework of Timed Automata can be used to determine valid parameter ranges for timers in logic control programs. The procedure is illustrated by means of a simple process engineering example for which the complete Timed Automata model is presented. To analyse the model, the tool HyTech is used which provides routines to determine values of model parameters depending on. reachability conditions. (C) 1998 Elsevier Science Ltd. All rights reserved.

引用

页码：S875 / S878

页数：4

共 50 条

[1] Model-checking for weighted timed automata
Brihaye, T
Bruyère, V
Raskin, JF
[J]. FORMAL TECHNIQUES, MODELLING AND ANALYSIS OF TIMED AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS, 2004, 3253 : 277 - 292
[2] Model-checking timed automata with deadlines with Uppaal
Gomez, Rodolfo
[J]. FORMAL ASPECTS OF COMPUTING, 2013, 25 (02) : 289 - 318
[3] Weighted Timed Automata: Model-Checking and Games
Bouyer, Patricia
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 158 : 3 - 17
[4] On model-checking timed automata with stopwatch observers
Brihaye, T
Bruyére, V
Raskin, JFO
[J]. INFORMATION AND COMPUTATION, 2006, 204 (03) : 408 - 433
[5] Durations and parametric model-checking in timed automata
Bruyere, Veronique
Dall'olio, Emmanuel
Raskin, Jean-Francois
[J]. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2008, 9 (02)
[6] Mapping OWL-S Process Model to Timed Automata: A Model-Checking Timed Temporal Logic Oriented Approach
Boumaza, Amel
Maamri, Ramdane
[J]. JOURNAL OF INFORMATION TECHNOLOGY RESEARCH, 2018, 11 (01) : 29 - 48
[7] Model-checking one-clock priced timed automata
Bouyer, Patricia
Larsen, Kim G.
Markey, Nicolas
[J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2007, 4423 : 108 - 122
[8] Durations, parametric model-checking in timed automata with Presburger arithmetic
Bruyère, V
Dall'Olio, E
Raskin, JF
[J]. STACS 2003, PROCEEDINGS, 2003, 2607 : 687 - 698
[9] Formal Specification and Model-Checking of CSMA/CA Using Finite Precision Timed Automata
LI Liang~(1
2. Lab of Computer Science
[J]. The Journal of China Universities of Posts and Telecommunications, 2005, (03) : 33 - 38
[10] Robust model-checking of linear-time properties in timed automata
Bouyer, P
Markey, N
Reynier, PA
[J]. LATIN 2006: THEORETICAL INFORMATICS, 2006, 3887 : 238 - 249

← 1 2 3 4 5 →