Formal Verification of Downtimeless System Evolution in Embedded Automation Controllers

被引：16
|
作者：
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 条
  • [1] Towards an approach for the verification of downtimeless system evolution
    Suender, Christoph
    Favre-Bulle, Bernard
    Vyatkin, Valeriy
    [J]. 2006 IEEE CONFERENCE ON EMERGING TECHNOLOGIES & FACTORY AUTOMATION, VOLS 1 -3, 2006, : 1203 - +
  • [2] Formal verification for embedded system designs
    Chen, X
    Hsieh, H
    Balarin, F
    Watanabe, Y
    [J]. DESIGN AUTOMATION FOR EMBEDDED SYSTEMS, 2003, 8 (2-3) : 139 - 153
  • [3] Formal Verification for Embedded System Designs
    Xi Chen
    Harry Hsieh
    Felice Balarin
    Yosinori Watanabe
    [J]. Design Automation for Embedded Systems, 2003, 8 : 139 - 153
  • [4] Formal Hardware/Software Co-Verification of Embedded Power Controllers
    Dasgupta, Pallab
    Srivas, Mandayam K.
    Mukherjee, Rajdeep
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2014, 33 (12) : 2025 - 2029
  • [5] Formal verification of sequence controllers
    Park, T
    Barton, PI
    [J]. COMPUTERS & CHEMICAL ENGINEERING, 2000, 23 (11-12) : 1783 - 1793
  • [6] Formal specification and verification of embedded system with shared resources
    Bang, KS
    Choi, JY
    Jang, SH
    [J]. 15TH IEEE INTERNATIONAL WORKSHOP ON RAPID SYSTEM PROTOTYPING, PROCEEDINGS: SHORTENING THE PATH FROM SPECIFICATION TO PROTOTYPE, 2004, : 8 - 14
  • [7] Specification and formal verification of safety properties in a point automation system
    Sener, Ibrahim
    Kaymakci, Ozgur Turay
    Ustoglu, Ilker
    Cansever, Galip
    [J]. TURKISH JOURNAL OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCES, 2016, 24 (03) : 1384 - 1396
  • [8] A Framework for Formal Verification of DRAM Controllers
    Steiner, Lukas
    Sudarshan, Chirag
    Jung, Matthias
    Stoffel, Dominik
    Wehn, Norbert
    [J]. PROCEEDINGS OF THE INTERNATIONAL SYMPOSIUM ON MEMORY SYSTEMS, MEMSYS 2022, 2022,
  • [9] Formal Verification of Grid Frequency Controllers
    Mohapatra, Anurag
    Peric, Vedran S.
    Hamacher, Thomas
    [J]. 2021 IEEE PES INNOVATIVE SMART GRID TECHNOLOGY EUROPE (ISGT EUROPE 2021), 2021, : 643 - 648
  • [10] Formal verification of embedded SoC
    Wang, B
    Lin, ZH
    [J]. 2001 4TH INTERNATIONAL CONFERENCE ON ASIC PROCEEDINGS, 2001, : 769 - 772
12345