NDLI: Automated Formal Verification and Testing of C Programs for Embedded Systems

Content Provider	IEEE Xplore Digital Library
Author	Kandl, S. Kirner, R. Puschner, P.
Copyright Year	2007
Description	Author affiliation: Inst. fur Technische Informatik, Technische Univ. Wien (Kandl, S.; Kirner, R.; Puschner, P.)
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
Starting Page	373
Ending Page	381
File Size	243218
Page Count	9
File Format	PDF
ISBN	0769527655
DOI	10.1109/ISORC.2007.22
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2007-05-07
Publisher Place	Greece
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Formal verification Automatic testing System testing Embedded system Automata Arithmetic Software testing Embedded software Real time systems Application software
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Automatic analysis of embedded systems specified in Astral

Formal Semantics of the ProCom Real-Time Component Model

Timed Automata Model for Component-Based Real-Time Systems

Formal verification of the PATHO real-time operating system

Formal verification of the MetaH executive using linear hybrid automata

Model checking real-time component based systems with blackbox testing

Testing embedded real-time systems

Iterative Algorithms For Formal Verification Of Embedded Real-time Systems

Formal Specs Reuse with Embedded Systems Design Behavioral and Architectural Specifications in Real-Time Application Domains

Automated Formal Verification and Testing of C Programs for Embedded Systems

Similar Documents

Automatic analysis of embedded systems specified in Astral

Formal Semantics of the ProCom Real-Time Component Model

Timed Automata Model for Component-Based Real-Time Systems

Formal verification of the PATHO real-time operating system

Formal verification of the MetaH executive using linear hybrid automata

Model checking real-time component based systems with blackbox testing

Testing embedded real-time systems

Iterative Algorithms For Formal Verification Of Embedded Real-time Systems

Formal Specs Reuse with Embedded Systems Design Behavioral and Architectural Specifications in Real-Time Application Domains

Automated Formal Verification and Testing of C Programs for Embedded Systems