research-article

SMT-Based Context-Bounded Model Checking for Embedded Systems: Challenges and Future Trends

Authors:

Lucas C. Cordeiro,

Eddie B. de Lima FilhoAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 41, Issue 3

Pages 1 - 6

https://doi.org/10.1145/2934240.2934247

Published: 24 June 2016 Publication History

Abstract

The dependency on the correct functioning of embedded systems is rapidly growing, mainly due to their wide range of applications, such as micro-grids, automotive device control (e.g., airbag control), health care, surveillance, mobile devices, and consumer electronics. Their structures are becoming more and more complex and now require multi-core processors with scalable shared memory, in order to meet increasing computational power demands. As a consequence, reliability of embedded (distributed) software becomes a key issue during system development, which must be carefully addressed and assured. Normally, state-of-the-art verification methodologies for embedded systems generate test vectors (with constraints) and use assertion-based verification and highlevel processor models, during simulation; however, other additional challenges have been raised: the need for meeting time and energy constraints, handling concurrent software, dealing with platform restrictions, evaluating implementation-structure choices, and supporting new software architectures and legacy designs (usually written in low-level languages). The present paper discusses challenges, problems, and recent advances to ensure correctness and timeliness regarding embedded systems. Reliability issues, in the development of micro-grids and cyber-physical systems, are then considered, as a prominent (bounded) model checking application.

References

[1]

H. Kopetz: Real-Time Systems - Design Principles for Distributed Embedded Applications. Real-Time Systems Series, Springer, ISBN 978-1-4419-8236-0, pp. 1--376, 2011.

Digital Library

[2]

Xua X., Jiaa H., Wanga D., Yub D., Chiangc H.: Hierarchical energy management system for multi-source multi-product microgrids In: Renewable Energy, v. 78, pp. 621--630, 2015.

[3]

Lee E.: Cyber-physical Systems: Design Challenges. In: International Symposium on Object Oriented Real-Time Distributed Computing, pp. 363--369, 2008.

Digital Library

[4]

Lee E.: The Past, Present and Future of Cyber-Physical Systems: A Focus on Models. In: Sensors 15(3): pp. 4837--4869, 2015.

[5]

Groza A., Letia I., Goron A., Zaporojan S.: A formal approach for identifying assurance deficits in unmanned aerial vehicle software In: Progress in Systems Engineering, Springer, pp. 233--239, 2015.

[6]

Cordeiro L., Fischer B., Chen H., Marques-Silva J.: Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints. In: International Conference on Embedded Software and Systems, pp. 396--403, 2009.

Digital Library

[7]

Munir S., Stankovic J. A., Liang C.-J. M., Lin S.: Cyber Physical System Challenges for Human-in-the-Loop Control. In: 8th International Workshop on Feedback Computing, pp. 1--4, 2013.

[8]

Kroening D., Liang L., Melham T., Schrammel P., Tautschnig M.: Effective Verification of Low-Level Software with Nested Interrupts. In: Design, Automation and Test in Europe, pp. 229--234, 2015.

Digital Library

[9]

Biere A., Cimatti A., Clarke E., Zhu Y.: Symbolic Model Checking without BDDs. In: Tools and Algorithms for Construction and Analysis of Systems, LNCS 1579, pp. 193--207, 1999.

Digital Library

[10]

Biere A., Heule M., van Maaren H., Walsh T., eds.: Handbook of Satisfiability. Volume 185 of Frontiers in Artifcial Intelligence and Applications., IOS Press, 2009.

Digital Library

[11]

Barrett C., Sebastiani R., Seshia S.A., Tinelli C.: Satisfiability Modulo Theories. In: Volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, pp. 825--885, 2009.

[12]

Armando A., Mantovani J., Platania L.: Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers. In: SPIN Workshop on Model Checking Software, LNCS 3925, pp. 146--162, 2006.

Digital Library

[13]

Clarke E., Kroening D., Lerda F.: A Tool for Checking ANSI-C Programs. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS 2988, Springer Berlin Heidelberg, pp. 168--176, 2004.

[14]

Merz F., Falke S., Sinz C.: LLBMC: Bounded Model Checking of C and C++ Programs using a Compiler IR. In: International Conference on Verified Software: Theories, Tools, Experiments. LNCS 7152, pp. 146--161, 2012.

Digital Library

[15]

Cordeiro L., Fischer B.: Verifying Multi-threaded Software using SMT-based Context-Bounded Model Checking. In: International Conference on Software Engineering. pp. 331--340, 2011.

Digital Library

[16]

Ivanicic F., Shlyakhter I., Gupta A., Ganai, M.K.: Model Checking C Programs using F-Soft. In: International Conference on Computer Design: VLSI in Computers and Processors, pp. 297--308, 2005.

Digital Library

[17]

Cordeiro L., Fischer B., Marques-Silva J.: SMT-based Bounded Model Checking for Embedded ANSI-C Software. IEEE Trans. Software Eng. 38(4), pp. 957--974, 2012.

Digital Library

[18]

Eén, N., Sörensson, N.: Temporal Induction by Incremental SAT Solving. Electronic Notes in Theoretical Computer Science 89(4), pp. 543--560, 2003.

[19]

Sheeran M., Singh S., Stålmarck G.: Checking Safety Properties using Induction and a SAT-solver. In: International Conference on Formal Methods in Computer-Aided Design. Springer-Verlag, pp. 108--125, 2000.

Digital Library

[20]

Bradley A., Manna Z.: The calculus of computation - decision procedures with applications to verification. In: Springer, pp. I-XV, pp. 1--366, 2007.

Digital Library

[21]

ParisTech M.: PIPS: Automatic Parallelizer and Code Transformation Framework. Accessed 21 February 2016

[22]

Henry J., Monniaux D., Moy M.: PAGAI: A Path Sensitive Static Analyser. In: Electronic Notes in Theoretical Computer Science, pp. 15--25, 2012.

Digital Library

[23]

Gadelha M., Ismail H., Cordeiro L.: Handling Loops in Bounded Model Checking of C Programs via k-Induction. In: International Journal on Software Tools for Technology Transfer (to appear), 2015. http://dx.doi.org/10.1007/s10009-015-0407-9

[24]

Beyer D., Dangl M., Wendler P.: Boosting k-Induction with Continuously-Refined Invariants. In: International Conference on Computer-Aided Verification, LNCS 9206, pp. 622--640, 2015.

[25]

Brain M., Joshi S., Kroening D., Schrammel P.: Safety Verification and Refutation by k-Invariants and k-Induction. In: International Symposium on Static Analysis, LNCS 9291, pp. 145--161, 2015.

[26]

Rocha H., Ismail H., Cordeiro L., Barreto R.: Model Checking Embedded C Software using k-Induction and Invariants. V Brazilian Symposium on Computing Systems Engineering, pp. 90--95, 2015.

Digital Library

[27]

Donaldson A., Haller L., Kroening D., Rümmer, P.: Software Verification using k-Induction. In: International Symposium on Static Analysis. LNCS 6887, pp. 351--368, 2011.

Digital Library

[28]

Donaldson A., Kroening D., Rümmer P.: SCRATCH: A Tool for Automatic Analysis of DMA Races. In: ACM Symposium on Principles and Practice of Parallel Programming. ACM, pp. 311--312, 2011.

Digital Library

[29]

Große D., Le H., Drechsler R.: Induction-based Formal Verification of SystemC TLM Designs. In: International Workshop on Microprocessor Test and Verification, pp. 101--106, 2009.

Digital Library

[30]

Behrend J., Lettnin D., Gruenhage A., Ruf J., Kropf T., Rosenstiel W.: Scalable and Optimized Hybrid Verification of Embedded Software. In: J. Electronic Testing 31(2): pp. 151--166, 2015.

Digital Library

[31]

Ismail H., Bessa I., Cordeiro L., Lima Filho E., Chaves Filho J.: DSVerifier: A Bounded Model Checking Tool for Digital Systems. In: International SPIN Symposium on Model Checking of Software, LNCS 9232, pp. 126--131, 2015.

Digital Library

[32]

Lettnin D., Nalla P. K., Behrend J., Ruf J., Gerlach J., Kropf T., Rosenstiel W., Schönknecht V., Reitemeyer S.: Semiformal Verification of Temporal Properties in Automotive Hardware Dependent Software. In: Design, Automation and Test in Europe, pp. 1214--1217, 2009.

Digital Library

[33]

D. Beyer Status report on software verification -- (competition summary SV-COMP). In: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 8413, pp. 373--388, 2014.

[34]

D. Beyer: Software Verification and Verifiable Witnesses -- (Report on SV-COMP 2015). In: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 9035, pp. 401--416, 2015.

Digital Library

[35]

Inverso O., Tomasco E., Fischer B., La Torre S., Parlato G.: Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. In: International Conference on Computer-Aided Verification, LNCS 8559, pp. 585--602, 2014.

Digital Library

[36]

Ramalho M., Lopes M., Sousa F., Marques H., Cordeiro L., Fischer B.: SMT-Based Bounded Model Checking of C++ Programs. In: International Conference on Engineering of Computer-Based Systems, pp. 147--156, 2013.

Digital Library

[37]

Pereira P. Albuquerque H., Marques H., Silva I., Carvalho C., Santos V., Ferreira R., Cordeiro L.: Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking. In: ACM Symposium on Applied Computing, Software Verification and Testing Track, pp. 1648--1653, 2016.

Digital Library

[38]

Sousa F., Cordeiro L., Lima Filho E.: Bounded Model Checking of C++ Programs Based on the Qt Framework. In: Global Conference on Consumer Electronics, pp. 179--180, 2015.

[39]

J. Morse. Expressive and Efficient Bounded Model Checkingof Concurrent Software. University of Southampton, PhD Thesis, 2015.

[40]

Zheng M, Rogers M, Luo Z, Dwyer M, Siegel S. CIVL: Formal Verification of Parallel Programs. In: International Conference on Automated Software Engineering, pp. 830--835, 2015.

Digital Library

[41]

Grumberg O., Lerda F., Strichman O., Theobald M.: Proof-guided underapproximation-widening for multi-process systems. In: Symposium on Principles of Programming Languages, pp. 122--131, 2005.

Digital Library

[42]

K. McMillan: Widening and Interpolation. In: International Symposium on Static Analysis, LCNS 6887, pp. 1, 2011.

Digital Library

[43]

Bessa I., Abreu R., Cordeiro L., Filho J.: SMT-Based Bounded Model Checking of Fixed-Point Digital Controllers). In: Annual Conference of the Industrial Electronics Society, pp. 295--301, 2014.

[44]

Abreu R., Cordeiro L., Filho E.: Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking. In: XXXI Brazilian Symposium on Telecommunications, 2013. http://dx.doi.org/10.14209/sbrt.2013.57

[45]

Morse J., Cordeiro L., Nicole D., Fischer B.: Model Checking LTL Properties over ANSI-C Programs with Bounded Traces. In: Software and System Modeling 14(1): pp. 65--81, 2015.

Digital Library

[46]

Bessa I., Ismail H., Cordeiro L., Chaves Filho J.: Verification of Fixed-Point Digital Controllers Using Direct and Delta Forms Realizations. In: Design Automation for Embedded Systems (to appear), 2016.

Digital Library

[47]

Morse J., Cordeiro L., Nicole D., Fischer B.: Handling unbounded loops with ESBMC 1.20. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS 7795, Springer Berlin Heidelberg, pp. 619--622, 2013.

Digital Library

[48]

Morse J., Ramalho M., Cordeiro L., Nicole D., Fischer B.: ESBMC 1.22. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS 8413, Springer Berlin Heidelberg, pp. 405--407, 2014.

[49]

Kahlon V., Wang C., Gupta A.: Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. In: International Conference on Computer-Aided Verification, LNCS 5643, pp. 398--413, 2009.

Digital Library

[50]

Alves E., Cordeiro L., Lima Filho E.: Fault Localization in Multi-Threaded C Programs using Bounded Model Checking. In: Brazilian Symposium on Computing Systems Engineering, pp. 96--101, 2015.

Digital Library

[51]

Garcia M., Sousa F., Cordeiro, L., Lima Filho E.: ESBMCQtOM: A Bounded Model Checking Tool to Verify Qt Applications. In: International SPIN symposium on Model Checking of Software (to appear), 2016.

[52]

Beyer D., Dangl M., Dietsch D., Heizmann M., Stahlbauer A.: Witness validation and stepwise testification across software verifiers. In: ESEC/SIGSOFT Foundations of Software Engineering, pp. 721--733, 2015.

Digital Library

[53]

Rocha H., Barreto R., Cordeiro L., Dias Neto A.: Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples. In: International Conference on Integrated Formal Methods, LNCS 7321, pp. 128--142, 2012.

Digital Library

Cited By

Jana RDey SMondal ADasgupta P(2020)Automated planning for finding alternative bug tracesIET Computers & Digital Techniques10.1049/iet-cdt.2019.028314:6(322-335)Online publication date: 18-Sep-2020
https://doi.org/10.1049/iet-cdt.2019.0283
Alt LAsadi SChockler HEven Mendoza KFedyukovich GHyvärinen ASharygina N(2017)HiFrogProceedings, Part II, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020610.1007/978-3-662-54580-5_12(207-213)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54580-5_12

SMT-Based Context-Bounded Model Checking for Embedded Systems: Challenges and Future Trends

Recommendations

SMT-based bounded model checking for multi-threaded software in embedded systems
ICSE '10: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2

The transition from single-core to multi-core processors has made multi-threaded software an important subject over the last years in computer-aided verification. Model checkers have been successfully applied to discover subtle errors, but they suffer ...
SMT-Based Bounded Model Checking for Embedded ANSI-C Software
ASE '09: Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering

Propositional bounded model checking has been applied successfully to verify embedded software but is limited by the increasing propositional formula size and the loss of structure during the translation. These limitations can be reduced by encoding ...
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 41, Issue 3

May 2016

46 pages

ISSN:0163-5948

DOI:10.1145/2934240

Editor:
Michael Wing

Issue’s Table of Contents

Copyright © 2016 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 June 2016

Published in SIGSOFT Volume 41, Issue 3

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
150
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)2

Reflects downloads up to 09 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Jana RDey SMondal ADasgupta P(2020)Automated planning for finding alternative bug tracesIET Computers & Digital Techniques10.1049/iet-cdt.2019.028314:6(322-335)Online publication date: 18-Sep-2020
https://doi.org/10.1049/iet-cdt.2019.0283
Alt LAsadi SChockler HEven Mendoza KFedyukovich GHyvärinen ASharygina N(2017)HiFrogProceedings, Part II, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020610.1007/978-3-662-54580-5_12(207-213)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54580-5_12

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents