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 条

[21] A Controlled Experiment in Testing of Safety-Critical Embedded Software
Enoiu, Eduard P.
Causevic, Adnan
Sundmark, Daniel
Pettersson, Paul
2016 9TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST), 2016, : 1 - 11
[22] A software diversity model for embedded safety-critical system
Wang, Haifeng
Liang, Nan
PROCEEDINGS OF THE 2009 INTERNATIONAL CONFERENCE ON WIRELESS NETWORKS AND INFORMATION SYSTEMS, 2009, : 106 - 109
[23] SMT-based scenario verification for hybrid systems
Alessandro Cimatti
Sergio Mover
Stefano Tonetta
Formal Methods in System Design, 2013, 42 : 46 - 66
[24] SMT-Based Stability Verification of an Industrial Switched PI Control Systems
Basagiannis, Stylianos
Battista, Ludovico
Becchi, Anna
Cimatti, Alessandro
Giantamidis, Georgios
Mover, Sergio
Tacchella, Alberto
Tonetta, Stefano
Tsachouridis, Vassilios
2023 53RD ANNUAL IEEE/IFIP INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS WORKSHOPS, DSN-W, 2023, : 243 - 250
[25] SMT-Based Bounded Model Checking for Embedded ANSI-C Software
Cordeiro, Lucas
Fischer, Bernd
Marques-Silva, Joao
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2012, 38 (04) : 957 - 974
[26] SMT-Based Bounded Model Checking for Embedded ANSI-C Software
Cordeiro, Lucas
Fischer, Bernd
Marques-Silva, Joao
2009 IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 137 - 148
[27] Testing and verification of neural-network-based safety-critical control software: A systematic literature review
Zhang, Jin
Li, Jingyue
INFORMATION AND SOFTWARE TECHNOLOGY, 2020, 123
[28] SMT-based scenario verification for hybrid systems
Cimatti, Alessandro
Mover, Sergio
Tonetta, Stefano
FORMAL METHODS IN SYSTEM DESIGN, 2013, 42 (01) : 46 - 66
[29] Model-based software development - A Process for safety-critical embedded Systems
Kuschnerus, Dirk
Gerding, Michael
Bilgic, Attila
Musch, Thomas
ATP EDITION, 2012, (7-8): : 60 - 66
[30] SMT-Based Modeling and Verification of Cloud Applications
Zhang, Xiyue
Sun, Meng
SERVICES - SERVICES 2019, 2019, 11517 : 1 - 15

← 1 2 3 4 5 →