NDLI: Debugging formal specifications using simple counterstrategies

Content Provider	IEEE Xplore Digital Library
Author	Konighofer, R. Hofferek, G. Bloem, R.
Copyright Year	2009
Description	Author affiliation: Institute for Applied Information Processing and Communications (IAIK), Graz University of Technology (Konighofer, R.; Hofferek, G.; Bloem, R.)
Abstract	Deriving a formal specification from an informal design intent is an error-prone process. The resulting specification may be incomplete, unrealizable, or in conflict with the design intent. We propose a debugging method for incorrect specifications that does not need an implementation. We show that we can explain conflicts with the design intent by explaining unrealizability. Our approach for explaining unrealizability is based on counterstrategies. Since counterstrategies may be large, we propose several ways to simplify them. First, we simplify the specification itself by removing both requirements and variables that do not contribute to the problem. Second, we heuristically search for a countertrace, i.e., a single input trace that suffices to demonstrate unrealizability. Finally, we present the countertrace or the counterstrategy to the user in extensive form as a graph and implicitly as an interactive game. We present experimental results for specifications given as GR(1) formulas.
Starting Page	152
Ending Page	159
File Size	214335
Page Count	8
File Format	PDF
ISBN	9781424449668
DOI	10.1109/FMCAD.2009.5351127
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2009-11-15
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Design engineering Protocols Debugging Information processing Computer errors Safety Formal specifications
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

Debugging formal specifications using simple counterstrategies (2009).

Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies

Survey of formal description techniques (FDTs) for protocol converter design

Design and Formal Specification of an X.25 Packet Level Protocol Implementation

TOGO-generating communication protocol implementations from formal specifications

Protocol engineering for application layer protocols

Parallel program debugging

Local Causal Reasoning of a Safety-Critical Subway System

A translation method from natural language specifications into formal specifications using contextual dependencies

Debugging formal specifications using simple counterstrategies

Similar Documents

Debugging formal specifications using simple counterstrategies (2009).

Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies

Survey of formal description techniques (FDTs) for protocol converter design

Design and Formal Specification of an X.25 Packet Level Protocol Implementation

TOGO-generating communication protocol implementations from formal specifications

Protocol engineering for application layer protocols

Parallel program debugging

Local Causal Reasoning of a Safety-Critical Subway System

A translation method from natural language specifications into formal specifications using contextual dependencies

Debugging formal specifications using simple counterstrategies