NDLI: Assumption generation for software component verification

Content Provider	IEEE Xplore Digital Library
Author	Giannakopoulou, D. Pasareanu, C.S. Barringer, H.
Copyright Year	2002
Description	Author affiliation: NASA Ames Res. Center, Moffett Field, CA, USA (Giannakopoulou, D.; Pasareanu, C.S.)
Abstract	Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. The typical approach to verifying properties of software components is to check them for all possible environments. In reality, however, a component is only required to satisfy properties in specific environments. Unless these environments are formally characterized and used during verification (assume-guarantee paradigm), the results returned by verification can be overly pessimistic. This work defines a framework that brings a new dimension to model checking of software components. When checking a component against a property, our model checking algorithms return one of the following three results: the component satisfies a property for any environment; the component violates the property for any environment; or finally, our algorithms generate an assumption that characterizes exactly those environments in which the component satisfies its required property. Our approach has been implemented in the LTSA tool and has been applied to the analysis of a NASA application.
Sponsorship	IEEE Comput. Soc. Tech. Committee on Software Eng. ACM SIGART ACM SIGSOFT Scottish Embedded Software Centre QinetiQ
Starting Page	3
Ending Page	12
File Size	329036
Page Count	10
File Format	PDF
ISBN	0769517366
ISSN	19384300
DOI	10.1109/ASE.2002.1114984
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2002-09-23
Publisher Place	UK
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	NASA Character generation Embedded software Space technology Computer science Application software Humans Operating systems Explosions Software systems
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

Component-based hardware/software co-verification

Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking

Model-based system development for embedded mobile platforms

Component-based approach to run-time kernel specification and verification

Assumption Generation for Software Component Verification (2002)

New directions in compiler technology for embedded systems

A HAL for component-based embedded operating systems

Assumption generation for software component verification (2002)

Assume-guarantee verification of source code with design-level assumptions

Assumption generation for software component verification

Similar Documents

Component-based hardware/software co-verification

Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking

Model-based system development for embedded mobile platforms

Component-based approach to run-time kernel specification and verification

Assumption Generation for Software Component Verification (2002)

New directions in compiler technology for embedded systems

A HAL for component-based embedded operating systems

Assumption generation for software component verification (2002)

Assume-guarantee verification of source code with design-level assumptions

Assumption generation for software component verification