Debugging Relational Declarative Models with Discriminating Examples
MetadataShow full item record
Models, especially those with mathematical or logical foundations, have proven valuable to engineering practice in a wide range of disciplines, including software engineering. Models, sometimes also referred to as logical specifications in this context, enable software engineers to focus on essential abstractions, while eliding less important details of their software design. Like any human-created artifact, a model might have imperfections at certain stages of the design process: it might have internal inconsistencies, or it might not properly express the engineer’s design intentions. Validating that the model is a true expression of the engineer’s intent is an important and difficult problem. One of the key challenges is that there is typically no other written artifact to compare the model to: the engineer’s intention is a mental object. One successful approach to this challenge has been automated example-generation tools, such as the Alloy Analyzer. These tools produce examples (satisfying valuations of the model) for the engineer to accept or reject. These examples, along with the engineer’s judgment of them, serve as crucial written artifacts of the engineer’s true intentions. Examples, like test-cases for programs, are more valuable if they reveal a discrepancy between the expressed model and the engineer’s design intentions. We propose the idea of discriminating examples for this purpose. A discriminating example is synthesized from a combination of the engineer’s expressed model and a machine-generated hypothesis of the engineer’s true intentions. A discriminating example either satisfies the model but not the hypothesis, or satisfies the hypothesis but not the model. It shows the difference between the model and the hypothesized alternative. The key to producing high-quality discriminating examples is to generate high-quality hypotheses. This dissertation explores three general forms of such hypotheses: mistakes that happen near borders; the expressed model is stronger than the engineer intends; or the expressed model is weaker than the engineer intends. We additionally propose a number of heuristics to guide the hypothesis-generation process. We demonstrate the usefulness of discriminating examples and our hypothesis-generation techniques through a case study of an Alloy model of Dijkstra’s Dining Philosophers problem. This model was written by Alloy experts and shipped with the Alloy Analyzer for several years. Previous researchers discovered the existence of a bug, but there has been no prior published account explaining how to fix it, nor has any prior tool been shown effective for assisting an engineer with this task. Generating high-quality discriminating examples and their underlying hypotheses is computationally demanding. This dissertation shows how to make it feasible.
Cite this version of the work
Vajihollah Montaghami (2017). Debugging Relational Declarative Models with Discriminating Examples. UWSpace. http://hdl.handle.net/10012/11288
Showing items related by title, author, creator and subject.
Zayan, Dina (University of Waterloo, 2013-12-03)We present a controlled experiment for the empirical evaluation of Example-Driven Modeling (EDM), an approach that systematically uses examples for model comprehension and domain knowledge transfer. We conducted the ...
Importance of regional variation in conservation planning: a rangewide example of the Greater Sage‐Grouse Doherty, Kevin E.; Evans, Jeffrey S.; Coates, Peter S.; Juliusson, Lara M.; Fedy, Bradley C. (Ecological Society of America, 2016-10-13)Abstract We developed rangewide population and habitat models for Greater Sage?Grouse (Centrocercus urophasianus) that account for regional variation in habitat selection and relative densities of birds for use in conservation ...
Fingerprinting and tracing the signature of basement-hosted unconformity-type uranium alteration through thick Quaternary tills: an example from the Thelon Basin, Nunavut Bustard, Aaron (University of Waterloo, 2016-05-17)The question of whether or not it is possible to trace the signature of alteration haloes surrounding deep-seated unconformity-type U mineralization through thick Quaternary tills is one of great importance for those ...