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 条
  • [21] AXIOMATIC SPECIFICATION AND LOGIC PROGRAMMING - FAST PROTOTYPING OF CORRECT DESIGNS
    BORIANI, DV
    ISA TRANSACTIONS, 1995, 34 (01) : 53 - 65
  • [22] Temporal logic and model checking
    McMillan, KL
    VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 36 - 54
  • [23] Model Checking of Spatial Logic
    Li, Tengfei
    Liu, Jing
    Kang, JieXiang
    Sun, Haiying
    Chen, Xiaohong
    Han, Li
    2020 27TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2020), 2020, : 169 - 177
  • [24] Temporal logic model checking
    Clarke, EM
    LOGIC PROGRAMMING - PROCEEDINGS OF THE 1997 INTERNATIONAL SYMPOSIUM, 1997, : 3 - 3
  • [25] Model Checking for Deontic Logic
    Koo, Jarok
    IFOST 2008: PROCEEDING OF THE THIRD INTERNATIONAL FORUM ON STRATEGIC TECHNOLOGIES, 2008, : 300 - 302
  • [26] Concurrency, logic, model checking
    Gerard, S
    Kozsik, T
    Pons, C
    Qiu, W
    Zhang, XG
    OBJECT-ORIENTED TECHNOLOGY: ECOOP'98 WORKSHOP READER, 1998, 1543 : 13 - 19
  • [27] Model checking for hybrid logic
    Lange M.
    Journal of Logic, Language and Information, 2009, 18 (4) : 465 - 491
  • [28] Generating Counterexamples for Model Checking by Transformation
    Hamilton, G. W.
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (216): : 65 - 82
  • [29] Towards a specification theory for fuzzy modal logic
    Jain, Manisha
    Gomes, Leandro
    Madeira, Alexandre
    Barbosa, Luis S.
    2021 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2021), 2021, : 175 - 182
  • [30] Towards evolvable analog fuzzy logic controllers
    do Amaral, JFM
    do Amaral, JLM
    Santini, CC
    Tanscheit, R
    Vellasco, MMR
    Pacheco, MAC
    2002 NASA/DOD CONFERENCE ON EVOLABLE HARDWARE, PROCEEDINGS, 2002, : 123 - 128
12345