18/2007 : Automated Formal Verification and Testing of C Programs for Embedded Systems

RR Number

18/2007

Conference

10th IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC'07)

Author(s)

Susanne Kandl, Peter Puschner

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.

Bibtex

@InProceedings{Kandl:ISORC2007,
  author =       {Susanne Kandl and Raimund Kirner and Peter Puschner},
  title =        {Automated Formal Verification and Testing of {C} Programs for Embedded Systems},
  booktitle =    {accepted for the 10th IEEE International Symposium on Object-Oriented
                  Real-Time Distributed Computing (ISORC'07)},
  year =         {2007},
  address =      {Santorin, Greece},
  month =        {May}
}

Download

Get kandl_AutFormVerifCES.pdf - Adobe PDF-format, (226.14 KB; posted at October 18 2010; )