SMT-Based Verification of Safety-Critical Embedded Control Software

被引：1
|
作者：
Adhikary, Sunandan [1 ]
Gurung, Amit [2 ]
Thakkar, Jay [3 ]
Da Costa, Antonio Bruto [1 ]
Dey, Soumyajit [1 ]
Hazra, Aritra [1 ]
Dasgupta, Pallab [1 ]
机构：
[1] Indian Inst Technol Kharagpur, Dept Comp Sci & Engn, Kharagpur 721302, W Bengal, India
[2] Martin Luther Christian Univ, Dept Comp Sci, Shillong 793006, Meghalaya, India
[3] Indian Inst Technol Gandhinagar, Ctr Creat Learning, Palaj 382355, India
来源：
IEEE EMBEDDED SYSTEMS LETTERS | 2021年 / 13卷 / 03期
关键词：
delta-approximation; control software verification; sampled data systems;
D O I：
10.1109/LES.2020.3035560
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
A large fraction of bugs discovered in the design flow of embedded control software (ECS) arises from the control software's interaction with the plant it controls. Traditional formal analysis approaches using interleaved controller-plant reach-set analysis grossly overapproximate the reachable states and does not scale. In this letter, we examine a verification approach that considers a control system with the (possibly nonlinear) plant dynamics and mode switches specified along with the actual control software implementation. Given this input, we generate a bounded-time safety verification problem encoded as satisfiability modulo theories (SMTs) constraints. We leverage delta-decidability over Reals to achieve scalability while verifying the control software.
引用
收藏
页码：138 / 141
页数：4
相关论文
共 50 条
  • [41] Model-Driven Engineering and Safety-Critical Embedded Software
    Shukla, Sandeep K.
    COMPUTER, 2009, 42 (09) : 93 - 95
  • [42] Cost-effective development of safety-critical embedded software
    Automotive Industries AI, 2007, 187 (04):
  • [43] Component-Based Modeling and Verification of Dynamic Adaptation in Safety-Critical Embedded Systems
    Adler, Rasmus
    Schaefer, Ina
    Trapp, Mario
    Poetzsch-Heffter, Arnd
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2010, 10 (02)
  • [44] A model-based Software Development Process for Safety-critical embedded Systems in industrial Measurement Technology UML-Framework for the Modeling of safety-critical Software
    Kuschnerus, Dirk
    Gerding, Michael
    Bilgic, Attila
    Musch, Thomas
    AUTOMATION 2012, 2012, 2171 : 55 - 58
  • [45] Efficient SMT-Based Network Fault Tolerance Verification
    Liu, Yu
    Subotic, Pavle
    Letier, Emmanuel
    Mechtaev, Sergey
    Roychoudhury, Abhik
    FORMAL METHODS, FM 2023, 2023, 14000 : 92 - 100
  • [46] SMT-Based Architecture Modelling for Safety Assessment
    Delmas, Kevin
    Delmas, Remi
    Pagetti, Claire
    2017 12TH IEEE INTERNATIONAL SYMPOSIUM ON INDUSTRIAL EMBEDDED SYSTEMS (SIES), 2017, : 166 - 173
  • [47] An SMT-Based Approach to the Verification of Knowledge-Based Programs
    Belardinelli, Francesco
    Boureanu, Ioana
    Malvone, Vadim
    Rajaona, Fortunat
    FORMAL ASPECTS OF COMPUTING, 2025, 37 (01)
  • [48] SMT-Based Formal Verification of a TTEthernet Synchronization Function
    Steiner, Wilfried
    Dutertre, Bruno
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, 2010, 6371 : 148 - +
  • [49] Software reliability analysis for safety-critical and control systems
    Kumar, Pramod
    Singh, Lalit Kumar
    Kumar, Chiranjeev
    QUALITY AND RELIABILITY ENGINEERING INTERNATIONAL, 2020, 36 (01) : 340 - 353
  • [50] Reliability demonstration testing method for safety-critical embedded applications software
    Qin, Zhidong
    Chen, Hui
    Shi, Youqun
    PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE AND SYSTEMS, 2008, : 481 - 487
12345