Model checking: Towards generating a correct specification for logic controllers

被引：0
|
作者：
Weng, XY [1 ]
Litz, L [1 ]
机构：
[1] Univ Kaiserslautern, Inst Proc Automat, D-67663 Kaiserslautern, Germany
来源：
PROCEEDINGS OF THE 2002 AMERICAN CONTROL CONFERENCE, VOLS 1-6 | 2002年 / 1-6卷
关键词：
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
PLC is widely used in industrial automation systems. Because of the increasing complexity in such systems, new methods for software specification and verification are needed to improve the reliability of these systems. Formal methods provide promising approaches to achieve this. In this contribution, relevant criteria are proposed to get a correct specification of PLC controllers using Signal Interpreted Petri Net (SIPN) framework. The temporal logic forms of these criteria are presented, so that model checking can be applied to verify the correctness of an SIPN design.
引用
收藏
页码：4457 / 4462
页数：6
相关论文
共 50 条
  • [41] Model checking linear logic specifications
    Bozzano, M
    DelZanno, G
    Martelli, M
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2004, 4 : 573 - 619
  • [42] A Study on the Model Checking for Deontic Logic
    Koo, Jarok
    Third 2008 International Conference on Convergence and Hybrid Information Technology, Vol 2, Proceedings, 2008, : 832 - 835
  • [43] UTP and Temporal Logic Model Checking
    Anderson, Hugh
    Ciobanu, Gabriel
    Freitas, Leo
    UNIFYING THEORIES OF PROGRAMMING, 2010, 5713 : 22 - +
  • [44] Model Checking Using Description Logic
    Ben-David, Shoham
    Trefler, Richard
    Weddell, Grant
    JOURNAL OF LOGIC AND COMPUTATION, 2010, 20 (01) : 111 - 131
  • [45] Model checking interval temporal logic
    Zhang, Hai-Bin
    Duan, Zhen-Hua
    Xi'an Dianzi Keji Daxue Xuebao/Journal of Xidian University, 2009, 36 (02): : 338 - 342
  • [46] Model Checking a Logic for True Concurrency
    Baldan, Paolo
    Padoan, Tommaso
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2020, 21 (04)
  • [47] Model checking distributed temporal logic
    Dionisio, Francisco
    Ramos, Jaime
    Subtil, Fernando
    Vigano, Luca
    LOGIC JOURNAL OF THE IGPL, 2024,
  • [48] Techniques for temporal logic model checking
    Deharbe, David
    REFINEMENT TECHNIQUES IN SOFTWARE ENGINEERING, 2006, 3167 : 315 - 367
  • [49] MCK: Model checking the logic of knowledge
    Gammie, P
    van der Meyden, R
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 479 - 483
  • [50] A logic of probability with decidable model checking
    Beauquier, Daniele
    Rabinovich, Alexander
    Slissenko, Anatol
    JOURNAL OF LOGIC AND COMPUTATION, 2006, 16 (04) : 461 - 487
12345