NDLI: Constrained-based symbolic execution on virtual models for functional coverage verification

Content Provider	IEEE Xplore Digital Library
Author	Mohamed, N.M. Wahba, A. Safar, M. Salem, A.
Copyright Year	2015
Description	Author affiliation: Comput. Eng. & Syst. Dept., Ain Shams Univ., Cairo, Egypt (Wahba, A.; Safar, M.) \|\| Design Verification Technol., Mentor Graphics, Cairo, Egypt (Mohamed, N.M.; Salem, A.)
Abstract	In this paper, we present a new approach for automatic test case generation with symbolic execution on virtual model. The test case generation is based on the concept of constrained-based and assertion-based techniques. We use the constrained-based technique in order to show preferences for the generated test cases and to obtain the desired goal of functional coverage. Basic idea of our technique is generating test cases from assertions. We used the assertion functions of the symbolic executor tool KLEE. With such setting, KLEE will carry out the virtual model through different paths in order to reach the assertion. Hence, the related test cases will validate the coverage of the assertion. To trigger the device to go through several states, we developed an additional method based on special functional coverage criteria. We present preliminary results on the test cases generation using a case study from ARM QEMU models. Our experimental results show that the proposed approach is efficient.
Sponsorship	Ain Shams Univ.
Starting Page	99
Ending Page	104
File Size	398215
Page Count	6
File Format	PDF
e-ISBN	9781467399715
DOI	10.1109/ICCES.2015.7393027
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2015-12-23
Publisher Place	Egypt
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Adaptation models KLEE Computational modeling Memory management Random access memory QEMU Hardware Software Explosions Virtual model Symbolic execution
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 test pattern generation for virtual hardware model using constrained symbolic execution

Distributed symbolic execution for binary software testing

Component-Based Model for Simulating the MMU CoProcessor

Ultra-Fast DMAC TLM Model for High Speed Virtual Platform Simulation

Enabling TLM-2.0 interface on QEMU and SystemC-based virtual platform

Coverage driven methodology for verification of soc hardware and software corner cases.

Disk Based Software Verification via Bounded Model Checking

A flexible modeling environment for a NoC-based multicore architecture

Formal hardware/software co-verification by interval property checking with abstraction

Constrained-based symbolic execution on virtual models for functional coverage verification

Similar Documents

Automatic test pattern generation for virtual hardware model using constrained symbolic execution

Distributed symbolic execution for binary software testing

Component-Based Model for Simulating the MMU CoProcessor

Ultra-Fast DMAC TLM Model for High Speed Virtual Platform Simulation

Enabling TLM-2.0 interface on QEMU and SystemC-based virtual platform

Coverage driven methodology for verification of soc hardware and software corner cases.

Disk Based Software Verification via Bounded Model Checking

A flexible modeling environment for a NoC-based multicore architecture

Formal hardware/software co-verification by interval property checking with abstraction

Constrained-based symbolic execution on virtual models for functional coverage verification