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 条
  • [31] Towards a tolerance representation model for generating tolerance specification schemes and corresponding tolerance zones
    Lu, Wenlong (hustwenlong@mail.hust.edu.cn), 1801, Springer London (97): : 5 - 8
  • [32] Towards a tolerance representation model for generating tolerance specification schemes and corresponding tolerance zones
    Yuchu Qin
    Wenlong Lu
    Qunfen Qi
    Xiaojun Liu
    Meifa Huang
    Paul J. Scott
    Xiangqian Jiang
    The International Journal of Advanced Manufacturing Technology, 2018, 97 : 1801 - 1821
  • [33] Towards a tolerance representation model for generating tolerance specification schemes and corresponding tolerance zones
    Qin, Yuchu
    Lu, Wenlong
    Qi, Qunfen
    Liu, Xiaojun
    Huang, Meifa
    Scott, Paul J.
    Jiang, Xiangqian
    INTERNATIONAL JOURNAL OF ADVANCED MANUFACTURING TECHNOLOGY, 2018, 97 (5-8): : 1801 - 1821
  • [34] Model checking embedded adaptive cruise controllers
    Nenchev, Vladislav
    ROBOTICS AND AUTONOMOUS SYSTEMS, 2023, 167
  • [35] The Formal Logic Approach for Checking the Observability of a Specification Language on DES Functioning
    Davydov, Artem
    Larionov, Aleksandr
    Nagul, Nadezhda
    2018 41ST INTERNATIONAL CONVENTION ON INFORMATION AND COMMUNICATION TECHNOLOGY, ELECTRONICS AND MICROELECTRONICS (MIPRO), 2018, : 938 - 943
  • [36] CTL formalized specification templates in model checking
    Chen, Z. (chenzhiyuan@hrbeu.edu.cn), 1600, Editorial Board of Journal of Harbin Engineering (34):
  • [37] Towards Combining Model Checking and Proof Checking
    Jiang, Ying
    Liu, Jian
    Dowek, Gilles
    Ji, Kailiang
    COMPUTER JOURNAL, 2019, 62 (09): : 1365 - 1402
  • [38] Petri net-based specification, analysis and synthesis of logic controllers
    Wegrzyn, A
    Wegrzyn, M
    PROCEEDINGS OF THE 2000 IEEE INTERNATIONAL SYMPOSIUM ON INDUSTRIAL ELECTRONICS, VOL 1 AND 2, 2000, : 20 - 26
  • [39] The Use of UML and Petri Net for Graphic Specification of the Reconfigurable Logic Controllers
    Bazydlo, Grzegorz
    Wojnakowski, Marcin
    Wisniewski, Remigiusz
    INTERNATIONAL CONFERENCE OF COMPUTATIONAL METHODS IN SCIENCES AND ENGINEERING 2018 (ICCMSE-2018), 2018, 2040
  • [40] Behavioral specification of the logic controllers by means of the hierarchical configurable Petri nets
    Doligalski, Michal
    11TH IFAC/IEEE INTERNATIONAL CONFERENCE ON PROGRAMMABLE DEVICES AND EMBEDDED SYSTEMS (PDES 2012), 2012,
12345