Content area
Full text
Int J Softw Tools Technol Transfer (2013) 15:563583 DOI 10.1007/s10009-011-0221-y
SYNTHESIS
Debugging formal specications: a practical approach using model-based diagnosis and counterstrategies
Robert Knighofer Georg Hofferek
Roderick Bloem
Published online: 16 December 2011 Springer-Verlag 2011
Abstract Creating a formal specication for a design is an error-prone process. At the same time, debugging incorrect specications is difcult and time consuming. In this work, we propose a debugging method for formal specications that does not require an implementation. We handle conicts between a formal specication and the informal design intent using a simulation-based renement loop, where we reduce the problem of debugging overconstrained specications to that of debugging unrealizability. We show how model-based diagnosis can be applied to locate an error in an unrealizable specication. The diagnosis algorithm computes properties and signals that can be modied in such a way that the specication becomes realizable, thus pointing out potential error locations. In order to x the specication, the user must understand the problem. We use counterstrategies to explain conicts in the specication. Since counterstrategies may be large, we propose several ways to simplify them. First, we compute the counterstrategy not for the original specication but only for an unrealizable core. Second, we use a heuristic to search for a countertrace, i.e., a single input trace which necessarily leads to a specication violation. Finally, we present the countertrace or the counterstrategy as an interactive game against the user, and as a graph summarizing possible plays of this game. We introduce a user-friendly implementation of our debugging method and present experimental results for GR(1) specications.
This work was supported in part by the European Commission through the projects COCONUT (FP7-2007-IST-1-217069) and DIAMOND (FP7-2009-IST-4-248613).
R. Knighofer (B) G. Hofferek R. Bloem
Institute for Applied Information Processing and Communications (IAIK), Graz University of Technology, Graz, Austriae-mail: [email protected]
Keywords Formal specication Debugging
Unrealizability Counterstrategies Model-based diagnosis
1 Introduction
Ideally, a formal specication for a design is written before the design is implemented. This establishes an unambiguous notion of correctness, which can be used as an objective during the implementation phase. It also makes the informal design intent precise, thus preventing misunderstandings between collaborating designers. Clearly, the specication must have the highest possible quality when used as correctness objective for the implementation. The...