| dc.contributor.author |
Adhikary, Sunandan |
|
| dc.contributor.author |
Gurung, Amit |
|
| dc.contributor.author |
Thakkar, Jay |
|
| dc.contributor.author |
Da Costa, Antonio Bruto |
|
| dc.contributor.author |
Dey, Soumyajit |
|
| dc.contributor.author |
Hazra, Aritra |
|
| dc.contributor.author |
Dasgupta, Pallab |
|
| dc.date.accessioned |
2020-12-02T15:27:05Z |
|
| dc.date.available |
2020-12-02T15:27:05Z |
|
| dc.date.issued |
2021-09 |
|
| dc.identifier.citation |
Adhikary, Sunandan; Gurung, Amit; Thakkar, Jay; Da Costa, Antonio Bruto; Dey, Soumyajit; Hazra, Aritra and Dasgupta, Pallab, “SMT-based verification of safety-critical embedded control software”, IEEE Embedded Systems Letters, DOI: 10.1109/LES.2020.3035560, vol. 13, no. 3, pp. 138-141, Sep. 2021. |
en_US |
| dc.identifier.issn |
1943-0663 |
|
| dc.identifier.issn |
1943-0671 |
|
| dc.identifier.uri |
https://doi.org/10.1109/LES.2020.3035560 |
|
| dc.identifier.uri |
https://repository.iitgn.ac.in/handle/123456789/5904 |
|
| dc.description.abstract |
A large fraction of bugs discovered in the design flow of Embedded Control Software (ECS) embedded control software arises from the control softwares interaction with the plant it controls. Traditional formal analysis approaches using interleaved controller-plant reach-set analysis grossly over-approximate the reachable states and does not scale. In this article, 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 (SMT) constraints. We leverage ?-decidability over Reals to achieve scalability while verifying the control software. |
|
| dc.description.statementofresponsibility |
by Sunandan Adhikary, Amit Gurung, Jay Thakkar, Antonio Bruto Da Costa, Soumyajit Dey, Aritra Hazra and Pallab Dasgupta |
|
| dc.format.extent |
vol. 13, no. 3, pp. 138-141 |
|
| dc.language.iso |
en_US |
en_US |
| dc.publisher |
Institute of Electrical and Electronics Engineers |
en_US |
| dc.subject |
Sampled Data Systems |
en_US |
| dc.subject |
?-Approximation |
en_US |
| dc.subject |
Control Software Verification |
en_US |
| dc.title |
SMT-based verification of safety-critical embedded control software |
en_US |
| dc.type |
Article |
en_US |
| dc.relation.journal |
IEEE Embedded Systems Letters |
|