Automated formal verification and testing of C programs for embedded systems

Susanne Kandl; Raimund Kirner; Peter Puschner

doi:10.1109/ISORC.2007.22

Automated formal verification and testing of C programs for embedded systems

Susanne Kandl, Raimund Kirner, Peter Puschner

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 Citations (Scopus)

36 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 language	English
Title of host publication	Procs of 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing
Editors	M DeMiguel, V Kalogeraki, DH Kim
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	373-382
Number of pages	9
ISBN (Print)	0-7695-2765-5
DOIs	https://doi.org/10.1109/ISORC.2007.22
Publication status	Published - 2007
Event	10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing - Santorini Isl Duration: 7 May 2007 → 9 May 2007

Conference

Conference	10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing
City	Santorini Isl
Period	7/05/07 → 9/05/07

Keywords

MODEL CHECKING
GENERATION

Access to Document

10.1109/ISORC.2007.22

905611
“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.”
Accepted author manuscript, 226 KB

Cite this

Kandl, S., Kirner, R., & Puschner, P. (2007). Automated formal verification and testing of C programs for embedded systems. In M. DeMiguel, V. Kalogeraki, & DH. Kim (Eds.), Procs of 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (pp. 373-382). Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/ISORC.2007.22

@inproceedings{7383bc1a377745488aebbb20c712bce7,

title = "Automated formal verification and testing of C programs for embedded systems",

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.",

keywords = "MODEL CHECKING, GENERATION",

author = "Susanne Kandl and Raimund Kirner and Peter Puschner",

note = "“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.”; 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing ; Conference date: 07-05-2007 Through 09-05-2007",

year = "2007",

doi = "10.1109/ISORC.2007.22",

language = "English",

isbn = "0-7695-2765-5",

pages = "373--382",

editor = "M DeMiguel and V Kalogeraki and DH Kim",

booktitle = "Procs of 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

address = "United States",

}

Kandl, S, Kirner, R & Puschner, P 2007, Automated formal verification and testing of C programs for embedded systems. in M DeMiguel, V Kalogeraki & DH Kim (eds), Procs of 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing. Institute of Electrical and Electronics Engineers (IEEE), pp. 373-382, 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing, Santorini Isl, 7/05/07. https://doi.org/10.1109/ISORC.2007.22

Automated formal verification and testing of C programs for embedded systems. / Kandl, Susanne; Kirner, Raimund; Puschner, Peter.
Procs of 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing. ed. / M DeMiguel; V Kalogeraki; DH Kim. Institute of Electrical and Electronics Engineers (IEEE), 2007. p. 373-382.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 - Institute of Electrical and Electronics Engineers (IEEE)

T2 - 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing

Y2 - 7 May 2007 through 9 May 2007

ER -

Automated formal verification and testing of C programs for embedded systems

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this