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 条
  • [21] Balancing Automation and Control for Formal Verification of Microprocessors
    Goel, Shilpi
    Slobodova, Anna
    Sumners, Rob
    Swords, Sol
    COMPUTER AIDED VERIFICATION (CAV 2021), PT I, 2021, 12759 : 26 - 45
  • [22] Modeling and formal verification of production automation systems
    Ruf, J
    Weiss, RJ
    Kropf, T
    Rosenstiel, W
    INTEGRATION OF SOFTWARE SPECIFICATION TECHNIQUES FOR APPLICATIONS IN ENGINEERING, 2004, 3147 : 541 - 566
  • [23] Formal verification of human-automation interaction
    Degani, A
    Heymann, M
    HUMAN FACTORS, 2002, 44 (01) : 28 - 43
  • [24] Verification and Synthesis of Timing Contracts for Embedded Controllers
    Al Khatib, Mohammad
    Girard, Antoine
    Dang, Thao
    HSCC'16: PROCEEDINGS OF THE 19TH INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2016, : 115 - 124
  • [25] The evolution of commercial formal verification
    Kurshan, RP
    PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V, 2000, : 2975 - 2980
  • [26] Using Visual Specifications in Verification of Industrial Automation Controllers
    Vyatkin, Valeriy
    Bouzon, Gustavo
    EURASIP JOURNAL ON EMBEDDED SYSTEMS, 2008, (01)
  • [27] Formal Modeling and Verification of Controllers for a Family of DRAM Caches
    Sahoo, Debiprasanna
    Sha, Swaraj
    Satpathy, Manoranjan
    Mutyam, Madhu
    Ramesh, S.
    Roop, Partha
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2018, 37 (11) : 2485 - 2496
  • [28] A formal verification technique for embedded software.
    Thiry, O
    Claesen, L
    INTERNATIONAL CONFERENCE ON COMPUTER DESIGN - VLSI IN COMPUTERS AND PROCESSORS, PROCEEDINGS, 1996, : 352 - 357
  • [29] Inference of Properties from Requirements and Automation of their Formal Verification
    Reich, Marina
    34TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2019), 2019, : 1222 - 1225
  • [30] A Runtime Verification Monitoring Approach for Embedded Industrial Controllers
    Watterson, Conal
    Heffernan, Donal
    2008 IEEE INTERNATIONAL SYMPOSIUM ON INDUSTRIAL ELECTRONICS, VOLS 1-5, 2008, : 853 - 858
12345