Formal Verification of Downtimeless System Evolution in Embedded Automation Controllers

被引：17
|
作者：
Suender, Christoph [1 ]
Vyatkin, Valeriy [2 ]
Zoitl, Alois [3 ]
机构：
[1] Thales Austria GmbH, A-1200 Vienna, Austria
[2] Univ Auckland, Auckland 1, New Zealand
[3] Vienna Univ Technol, Vienna, Austria
来源：
ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS | 2013年 / 12卷 / 01期
关键词：
Management; Verification; Standardization; Automation and control systems; dynamic reconfiguration; verification and validation; manufacturing automation; model checking; IEC; 61499; NCES; LOGIC CONTROLLERS; RECONFIGURATION;
D O I：
10.1145/2406336.2406353
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
This article presents a new formal approach to validation of on-the-fly modification of control software in automation systems. The concept of downtimeless system evolution (DSE) is introduced. The DSE is essentially based on the use of IEC 61499 system architecture and formal modeling and verification of the hardware and software of an automation device. The validation is performed by means of two complimentary techniques: analytic calculations and formal verification by model-checking.
引用
收藏
页数：17
相关论文
共 50 条
  • [41] Formal Verification for Embedded Systems Design Based on MDE
    Moreira do Nascimento, Francisco Assis
    da Silva Oliveira, Marcio Ferreira
    Wagner, Flavio Rech
    ANALYSIS, ARCHITECTURES AND MODELLING OF EMBEDDED SYSTEMS, 2009, 310 : 159 - +
  • [42] Formal Verification for Embedded Software with Cognitive Environment Modelling
    Meng, Qingdi
    Zhang, Lianyi
    Luo, Guiming
    2014 IEEE 13TH INTERNATIONAL CONFERENCE ON COGNITIVE INFORMATICS & COGNITIVE COMPUTING (ICCI-CC), 2014, : 355 - 360
  • [43] Specification and formal verification of temporal properties of production automation systems
    Flake, Stephan
    Müller, Wolfgang
    Pape, Ulrich
    Ruf, Jürgen
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2004, 3147 : 206 - 226
  • [44] Formal verification of a task scheduler for embedded operating systems
    Sun, Haiyong
    Lei, Hang
    JOURNAL OF INTELLIGENT & FUZZY SYSTEMS, 2020, 38 (02) : 1391 - 1399
  • [45] Specification and formal verification of temporal properties of production automation systems
    Flake, S
    Müller, W
    Pape, U
    Ruf, J
    INTEGRATION OF SOFTWARE SPECIFICATION TECHNIQUES FOR APPLICATIONS IN ENGINEERING, 2004, 3147 : 206 - 226
  • [46] Checking formal verification models for human-automation interaction
    van Paassen, M. M.
    Bolton, Matthew L.
    Jimenez, Noelia
    2014 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS (SMC), 2014, : 3709 - 3714
  • [47] Verification of embedded supervisory controllers considering hybrid plant dynamics
    Engell, S
    Lohmann, S
    Stursberg, O
    INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 2005, 15 (02) : 307 - 312
  • [48] Toward Automated Attack Discovery in SDN Controllers Through Formal Verification
    Yuan, Bin
    Zhang, Chi
    Ren, Jiajun
    Chen, Qunjinming
    Xu, Biang
    Zhang, Qiankun
    Li, Zhen
    Zou, Deqing
    Zhang, Fan
    Jin, Hai
    IEEE TRANSACTIONS ON NETWORK AND SERVICE MANAGEMENT, 2024, 21 (03): : 3636 - 3655
  • [49] Formal Verification of Neural Network Controllers for Collision-Free Flight
    Genin, Daniel
    Papusha, Ivan
    Brule, Joshua
    Young, Tyler
    Mullins, Galen
    Kouskoulas, Yanni
    Wu, Rosa
    Schmidt, Aurora
    SOFTWARE VERIFICATION, 2022, 13124 : 147 - 164
  • [50] Formal verification for analysis and design of logic controllers for reconfigurable machining systems
    Kalita, D
    Khargonekar, PP
    IEEE TRANSACTIONS ON ROBOTICS AND AUTOMATION, 2002, 18 (04): : 463 - 474
12345