TY - GEN
T1 - Automated formal verification and testing of C programs for embedded systems
AU - Kandl, Susanne
AU - Kirner, Raimund
AU - Puschner, Peter
N1 - “This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder."
“Copyright IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.”
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
KW - MODEL CHECKING
KW - GENERATION
U2 - 10.1109/ISORC.2007.22
DO - 10.1109/ISORC.2007.22
M3 - Conference contribution
SN - 0-7695-2765-5
SP - 373
EP - 382
BT - Procs of 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing
A2 - DeMiguel, M
A2 - Kalogeraki, V
A2 - Kim, DH
PB - IEEE
T2 - 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing
Y2 - 7 May 2007 through 9 May 2007
ER -