University of Hertfordshire

By the same authors

Automated formal verification and testing of C programs for embedded systems

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

Documents

  • 905611

    Accepted author manuscript, 226 KB, PDF document

View graph of relations
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
PublisherIEEE
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

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.

Notes

“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.”

ID: 323148