Automated formal verification and testing of C programs for embedded systems

Susanne Kandl, Raimund Kirner, Peter Puschner

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)
30 Downloads (Pure)

Abstract

In this paper, we introduce an approach for automated verification and testing of ANSI C programs for embedded systems. We automatically extract an automaton model from the C code of the SUT (system under test). This automaton model is on the one hand used for formal verification of the requirements defined in the system specification, on the other hand, we can derive test cases from this model, for both methods we use a model checker. We describe our techniques for test case generation, based on producing counterexamples with a model checker by formulating trap properties. The resulting test cases can then be applied to the SUT on different test levels. An important issue for model checking C-source code, is the correct modeling of the semantics of a C program for an embedded system. We focus on challenges and possible restrictions that appear, when model checking is used for the verification of C-source code. We specifically show how to deal with arithmetic expressions in the model checker NuSMV and how to preserve the numerical results in case of modeling the platform-specific semantics of C.
Original languageEnglish
Title of host publicationProcs of 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing
EditorsM DeMiguel, V Kalogeraki, DH Kim
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages373-382
Number of pages9
ISBN (Print)0-7695-2765-5
DOIs
Publication statusPublished - 2007
Event10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing - Santorini Isl
Duration: 7 May 20079 May 2007

Conference

Conference10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing
CitySantorini Isl
Period7/05/079/05/07

Keywords

  • MODEL CHECKING
  • GENERATION

Fingerprint

Dive into the research topics of 'Automated formal verification and testing of C programs for embedded systems'. Together they form a unique fingerprint.

Cite this