Skip to main content
SpringerLink
Log in
Book cover

Embedded Software Verification and Debugging pp 183–205Cite as

Scalable and Optimized Hybrid Verification of Embedded Software

  • Chapter
  • First Online:

  • 1593 Accesses

Part of the book series: Embedded Systems ((EMSY))

Abstract

The verification of embedded software has become an important subject over the last years. However, neither standalone verification approaches, like simulation-based/formal verification, nor state-of-the-art semiformal verification approaches are able to verify large and complex-embedded software with or without hardware dependencies. This work presents a scalable hybrid verification approach for the verification of embedded software using a semiformal algorithm optimized with static parameter assignment (SPA) . These algorithms and methodologies like SPA and counterexample guided simulation are used to combine simulation-based and formal verification in a new way. SPA offers a method to interact between dynamic and static verification approaches based on an automated ranking determination of possible function parameters according to the impact on the model size. Furthermore, SPA inserts initialization code for specific function parameters into the source code under test and supports model building and optimization algorithms to reduce the state space. We have successfully applied this optimized hybrid verification methodology to embedded software applications: Motorola’s Powerstone Benchmark suite and a complex automotive industrial embedded software. The results show that our approach scales better than standalone software model checkers to reach deep state spaces.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   129.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   139.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Jerraya AA, Yoo S, Verkest D, Wehn N (2003) Embedded software for SoC. Kluwer Academic Publishers, Norwell, MA, USA

    Book  MATH  Google Scholar 

  2. Beyer D, Henzinger TA, Jhala R, Majumdar R (2007) The software model checker BLAST: applications to software engineering. Int J Softw Tools Technol Trans

    Google Scholar 

  3. Behrend J, Lettnin D, Heckler P, Ruf J, Kropf T, Rosenstiel W (2011) Scalable hybrid verification for embedded software. In: DATE ’11: proceedings of the conference on design, automation and test in Europe, pp 1–6

    Google Scholar 

  4. Barrett C, Sebastiani R, Seshia SA, Tinelli C (2009) Satisfiability modulo theories. Frontiers in artificial intelligence and applications, Chap 26, vol 185. IOS Press, pp 825–885

    Google Scholar 

  5. Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Tools and algorithms for the construction and analysis of systems. Springer, pp 168–176

    Google Scholar 

  6. Kroening D (2009) Bounded model checking for ANSI-C. http://www.cprover.org/cbmc/

  7. Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. In: Zelkowitz M (ed) Highly dependable software. Advances in computers, vol 58. Academic Press

    Google Scholar 

  8. Cordeiro L, Fischer B, Marques-Silva J (2009) SMT-based bounded model checking for embedded ANSI-C software. In: ASE’09: proceedings of the 2009 IEEE/ACM international conference on automated software engineering. IEEE Computer Society, Washington, DC, pp 137–148

    Google Scholar 

  9. Ball T, Majumdar R, Millstein T, Rajamani SK (2001) Automatic predicate abstraction of C programs. SIGPLAN Not 36:203–213

    Article  Google Scholar 

  10. Flanagan C, Qadeer S (2002) Predicate abstraction for software verification. SIGPLAN Not 37:191–202

    Article  MATH  Google Scholar 

  11. Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50:752–794

    Article  MathSciNet  MATH  Google Scholar 

  12. Clarke E, Grumberg O, Long D (1994) Model checking and abstraction. ACM Trans Prog Lang syst 16(5):1512–1542

    Article  Google Scholar 

  13. Henzinger TA, Jhala R, Majumdar R (2005) The BLAST software verification system. Model Checking Softw 3639:25–26

    Google Scholar 

  14. Clarke E, Kroening D, Sharygina N, Yorav K (2005) SATABS: SAT-based predicate abstraction for ANSI-C. In: TACAS, vol 3440. Springer, pp 570–574

    Google Scholar 

  15. Gorai S, Biswas S, Bhatia L, Tiwari P, Mitra RS (2006) Directed-simulation assisted formal verification of serial protocol and bridge. In: DAC ’06: proceedings of the 43rd annual design automation conference. ACM, New York, pp 731–736

    Google Scholar 

  16. Nanshi K, Somenzi F (2006) Guiding simulation with increasingly refined abstract traces. In: DAC ’06: proceedings of the 43rd annual design automation conference. ACM, New York, pp 737–742

    Google Scholar 

  17. Di Guglielmo G, Fummi F, Pravadelli G, Soffia S, Roveri M (2010) Semi-formal functional verification by EFSM traversing via NuSMV. In: 2010 IEEE international High level design validation and test workshop (HLDVT), pp 58–65

    Google Scholar 

  18. Edwards SA, Ma T, Damiano R (2001) Using a hardware model checker to verify software. In: proceedings of the 4th international conference on ASIC (ASICON)

    Google Scholar 

  19. Lettnin D, Nalla PK, Behrend J, Ruf J, Gerlach J, Kropf T, Rosenstiel W, Schönknecht V, Reitemeyer S (2009) Semiformal verification of temporal properties in automotive hardware dependent software. In: DATE’09: proceedings of the conference on design, automation and test in Europe, pp 1214–1217

    Google Scholar 

  20. Ruf J, Peranandam PM, Kropf T, Rosenstiel W (2003) Bounded property checking with symbolic simulation. In: FDL

    Google Scholar 

  21. Cordeiro L, Fischer B, Chen H, Marques-Silva J (2009) Semiformal verification of embedded software in medical devices considering stringent hardware constraints. In: Second international conference on embedded software and systems, pp 396–403

    Google Scholar 

  22. Godefroid P, Klarlund N, Sen K (2005) Dart: directed automated random testing. SIGPLAN Not 40(6):213–223. http://doi.acm.org/10.1145/1064978.1065036

  23. Cadar C, Ganesh V, Pawlowski PM, Dill DL, Engler DR (2006) Exe: automatically generating inputs of death. In: Proceedings of the 13th ACM conference on computer and communications security. CCS’06. ACM, New York, pp 322–335. http://doi.acm.org/10.1145/1180405.1180445

  24. Sen K, Marinov D, Agha G (2005) CUTE: a concolic unit testing engine for C. SIGSOFT Softw Eng Notes 30(5):263–272. http://doi.acm.org/10.1145/1095430.1081750

  25. Di Guglielmo G, Fujita M, Fummi F, Pravadelli G, Soffia S (2011) EFSM-based model-driven approach to concolic testing of system-level design. In: 2011 9th IEEE/ACM international conference on formal methods and models for codesign (MEMOCODE), pp 201–209

    Google Scholar 

  26. Cadar C, Dunbar D, Engler D (2008) KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX conference on operating systems design and implementation. OSDI’08. USENIX Association, Berkeley, pp 209–224

    Google Scholar 

  27. Lattner C, Adve V (2005) The llvm compiler framework and infrastructure tutorial. In: Eigenmann R, Li Z, Midkiff S (eds) Languages and compilers for high performance computing. Lecture notes in computer science, vol 3602. Springer, Berlin, pp 15–16

    Google Scholar 

  28. Tillmann N, De Halleux J (2008) Pex: white box test generation for .net. In: Proceedings of the 2nd international conference on tests and proofs. TAP’08. Springer, Heidelberg, pp 134–153. http://dl.acm.org/citation.cfm?id=1792786.1792798

  29. Cuoq P, Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2012) Frama-C: a software analysis perspective. In: Proceedings of the 10th international conference on software engineering and formal methods. SEFM’12. Springer, Heidelberg, pp 233–247

    Google Scholar 

  30. Correnson L, Signoles J (2012) Combining analyses for C program verification. In: Stoelinga M, Pinger R (eds) Formal methods for industrial critical systems. Lecture notes in computer science, vol 7437. Springer, Berlin, pp 108–130

    Google Scholar 

  31. Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2015) Frama-C: a software analysis perspective. Formal Aspects Comput:1–37

    Google Scholar 

  32. Weiss RJ, Ruf J, Kropf T, Rosenstiel W (2005) Efficient and customizable integration of temporal properties into SystemC. In: Forum on specification & design languages (FDL), pp 271–282

    Google Scholar 

  33. Clarke E, Grumberg O, Hamaguchi K (1994) Another look at LTL model checking. In: Dill DL (ed) Conference on computer aided verification (CAV). Lecture notes in computer science, vol 818. Springer, Stanford, pp 415–427

    Google Scholar 

  34. Necula GC, McPeak S, Rahul SP, Weimer W (2002) CIL: intermediate language and tools for analysis and transformation of C programs. In: Computational complexity, pp 213–228

    Google Scholar 

  35. MISRA (2000) MISRA—the motor industry software reliability association. http://www.misra.org.uk/

  36. Shea R (2009) Call graph visualization for C and TinyOS programs. In: Department of computer science school of engineering UCLA. http://www.ambleramble.org/callgraph/index.html

  37. Lettnin D, Nalla PK, Ruf J, Kropf T, Rosenstiel W, Kirsten T, Schönknecht V, Reitemeyer S (2008) Verification of temporal properties in automotive embedded software. In: DATE’08: proceedings of the conference on design, automation and test in Europe. ACM, New York, pp 164–169

    Google Scholar 

  38. Open SystemC Initiative (2003) SystemC verification standard library 1.0p users manual

    Google Scholar 

  39. Clarke E, Kroening D, Yorav K (2003) Behavioral consistency of C and verilog programs using bounded model checking. In: DAC’03: proceedings of the 40th annual design automation conference. ACM, New York, pp 368–371

    Google Scholar 

  40. GNU (2010) Gcov coverage. http://gcc.gnu.org/onlinedocs/gcc/Gcov.html

  41. Malik A, Moyer B, Cermak D (2000) The M’CORE (TM) M340 unified cache architecture. In: Proceedings of the 2000 international conference on computer design, pp 577–580

    Google Scholar 

  42. NEC NEC Electronics (Europe) GmbH. http://www.eu.necel.com/

Download references

Acknowledgements

The authors would like to thank Edgar Auerswald, Patrick Koecher and Sebastian Welsch for supporting the development of the VERIFYR platform.

Author information

Authors and Affiliations

  1. Department of Computer Engineering, University of Tübingen, Sand 13, 72076, Tübingen, Germany

    Jörg Behrend, Alexander Grünhage, Jürgen Ruf, Thomas Kropf & Wolfgang Rosenstiel

  2. Department of Electrical and Electronic Engineering, Federal University of Santa Catarina, Campus Universitário s/n, Trindade, Florianópolis, SC, CEP 88040-900, Brazil

    Djones Lettnin

Authors
  1. Jörg Behrend
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Djones Lettnin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexander Grünhage
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jürgen Ruf
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Thomas Kropf
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Wolfgang Rosenstiel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jörg Behrend .

Editor information

Editors and Affiliations

  1. Universidade Federal de Santa Catarina, Florianópolis, Brazil

    Djones Lettnin

  2. Luzern, Switzerland

    Markus Winterholer

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer Science+Business Media, LLC

About this chapter

Cite this chapter

Behrend, J., Lettnin, D., Grünhage, A., Ruf, J., Kropf, T., Rosenstiel, W. (2017). Scalable and Optimized Hybrid Verification of Embedded Software. In: Lettnin, D., Winterholer, M. (eds) Embedded Software Verification and Debugging. Embedded Systems. Springer, New York, NY. https://doi.org/10.1007/978-1-4614-2266-2_8

Download citation

  • DOI: https://doi.org/10.1007/978-1-4614-2266-2_8

  • Published:

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4614-2265-5

  • Online ISBN: 978-1-4614-2266-2

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation