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 条

[31] Research on Formal Verification Technique for Aircraft Safety-Critical Software
Yin, Yongfeng
Liu, Bin
Su, Duo
JOURNAL OF COMPUTERS, 2010, 5 (08) : 1152 - 1159
[32] SOME VERIFICATION TOOLS AND METHODS FOR AIRBORNE SAFETY-CRITICAL SOFTWARE
HELPS, KA
SOFTWARE ENGINEERING JOURNAL, 1986, 1 (06): : 248 - 253
[33] Advances in modeling, verification and testing of safety-critical software architectures
Abderrahim Ait Wakrime
Yassine Ouhammou
Innovations in Systems and Software Engineering, 2022, 18 : 483 - 484
[34] A Compositional Verification Method for AADL Models of Safety-Critical Software
Zhang B.-L.
Yang Z.-B.
Zhou Y.
Ma Y.-Y.
Huang Z.-Q.
Xue L.
Jisuanji Xuebao/Chinese Journal of Computers, 2020, 43 (11): : 2134 - 2151
[35] Safety-critical software
1600, IEEE Computer Society (30):
[36] Safety-Critical Software
Merino, Pedro
Schoitsch, Erwin
ERCIM NEWS, 2008, (75): : 12 - 13
[37] SAFETY-CRITICAL SOFTWARE
PANCUCCI, D
ENGINEERING, 1991, 231 (08): : 45 - 47
[38] Advances in modeling, verification and testing of safety-critical software architectures
Ait Wakrime, Abderrahim
Ouhammou, Yassine
INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2022, 18 (04) : 483 - 484
[39] A Unifying View on SMT-Based Software Verification (vol 60, pg 299, 2018)
Beyer, Dirk
Dangl, Matthias
Wendler, Philipp
JOURNAL OF AUTOMATED REASONING, 2021, 65 (03) : 461 - 461
[40] Completeness in SMT-based BMC for software programs
Ganai, Malay K.
Gupta, Aarti
2008 DESIGN, AUTOMATION AND TEST IN EUROPE, VOLS 1-3, 2008, : 710 - 715

← 1 2 3 4 5 →