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 条
  • [41] LTL Model-Checking for Communicating Concurrent Programs
    Pommellet, Adrien
    Touili, Tayssir
    [J]. VERIFICATION AND EVALUATION OF COMPUTER AND COMMUNICATION SYSTEMS, 2018, 11181 : 150 - 165
  • [42] Symbolic model checking for probabilistic timed automata
    Kwiatkowska, Marta
    Norman, Gethin
    Sproston, Jeremy
    Wang, Fuzhi
    [J]. INFORMATION AND COMPUTATION, 2007, 205 (07) : 1027 - 1077
  • [43] Reachability analysis of pushdown automata: Application to model-checking
    Bouajjani, A
    Esparza, J
    Maler, O
    [J]. CONCUR'97 : CONCURRENCY THEORY, 1997, 1243 : 135 - 150
  • [44] MODEL-CHECKING OF ORDERED MULTI-PUSHDOWN AUTOMATA
    Atig, Mohamed Faouzi
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (03)
  • [45] Comparison of Model Checking Tools Using Timed Automata - PRISM and UPPAAL
    Naeem, Aaamir
    Azam, Farooque
    Amjad, Anam
    Anwar, Muhammad Waseem
    [J]. 2018 IEEE INTERNATIONAL CONFERENCE ON COMPUTER AND COMMUNICATION ENGINEERING TECHNOLOGY (CCET), 2018, : 248 - 253
  • [46] Model-checking timed ATL for durational concurrent game structures
    Laroussinie, Francois
    Markey, Nicolas
    Oreiby, Ghassan
    [J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2006, 4202 : 245 - 259
  • [47] Dealing with practical limitations of distributed timed model checking for timed automata
    V. Braberman
    A. Olivero
    F. Schapachnik
    [J]. Formal Methods in System Design, 2006, 29 : 197 - 214
  • [48] Improved algorithms for the automata-based approach to model-checking
    Doyen, Laurent
    Raskin, Jean-Francois
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 451 - +
  • [49] Model Checking Logic WCTL with Multi Constrained Modalities on One Clock Priced Timed Automata
    Chiplunkar, Ashish
    Krishna, Shankara Narayanan
    Jain, Chinmay
    [J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, PROCEEDINGS, 2009, 5813 : 88 - 102
  • [50] Model-checking access control policies
    Guelev, DP
    Ryan, M
    Schobbens, PY
    [J]. INFORMATION SECURITY, PROCEEDINGS, 2004, 3225 : 219 - 230
12345