NDLI: Interface Grammars for Modular Software Model Checking

Content Provider	IEEE Xplore Digital Library
Author	Hughes, G. Bultan, T.
Copyright Year	1976
Abstract	Verification techniques relying on state enumeration (e.g., model checking) face two important challenges: the state-space explosion, an exponential increase in the state space as the number of components increases; and environment generation, modeling components that are either not available for analysis, or that cannot be handled by the verification tool in use. We propose a semi-automated approach for attacking these problems. In our approach, interfaces for the components not under analysis are specified using a specification language based on grammars. Specifically, an interface grammar for a component specifies the sequences of method invocations that are allowed by that component. We have built an compiler that takes the interface grammar for a component as input and generates a stub for that component. The stub thus generated can be used to replace that component during state space exploration, either to moderate state space explosion, or to provide an executable environment for the component under verification. We conducted a case study by writing an interface grammar for the Enterprise JavaBeans (EJB) persistence interface, and using the resulting stub to check EJB clients using the JPF model checker. Our results show that EJB clients can be verified efficiently with JPF using our approach.
Sponsorship	IEEE Computer Society Technical Council on Software Engineering Association for Computing Machinery (ACM) IEEE Computer Society
Starting Page	614
Ending Page	632
Page Count	19
File Size	4917041
File Format	PDF
ISSN	00985589
Volume Number	34
Issue Number	5
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2008-09-01
Publisher Place	U.S.A.
Access Restriction	One Nation One Subscription (ONOS)
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	State-space methods Java Explosions Software tools Specification languages Space exploration Automata Production Writing Hardware modular verification Model checking Languages interface grammars
Content Type	Text
Resource Type	Article
Subject	Software

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

Modular Software Model Checking for Distributed Systems

An industrially effective environment for formal hardware verification

Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems

Symbolic Compilation of PSL

Automated Interface Refinement for Compositional Verification

Verification of NBS Class 4 Transport Protocol

SMT-Based Bounded Model Checking for Embedded ANSI-C Software

Tool support for verifying UML activity diagrams

Model checking agent programming languages

Interface Grammars for Modular Software Model Checking

Similar Documents

Modular Software Model Checking for Distributed Systems

An industrially effective environment for formal hardware verification

Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems

Symbolic Compilation of PSL

Automated Interface Refinement for Compositional Verification

Verification of NBS Class 4 Transport Protocol

SMT-Based Bounded Model Checking for Embedded ANSI-C Software

Tool support for verifying UML activity diagrams

Model checking agent programming languages

Interface Grammars for Modular Software Model Checking