*banner
 

Debugging Temporal Specifications with Concept Analysis
Glenn Ammons, David Mandelin, Rastislav Bodik, James Larus

Citation
Glenn Ammons, David Mandelin, Rastislav Bodik, James Larus. "Debugging Temporal Specifications with Concept Analysis". Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June, 2003.

Abstract
Program verification tools (such as model checkers and static analyzers) can find many errors in programs. These tools need formal specifications of correct program behavior, but writing a correct specification is difficult, just as writing a correct program is difficult. Thus, just as we need methods for debugging programs, we need methods for debugging specifications. This paper describes a novel method for debugging formal, temporal specifications. Our method exploits the short program execution traces that program verification tools generate from specification violations and that specification miners extract from programs. Manually examining these traces is a straightforward way to debug a specification, but this method is tedious and error-prone because there may be hundreds or thousands of traces to inspect. Our method uses concept analysis to automatically group the traces into highly similar clusters. By examining clusters instead of individual traces, a person can debug a specification with less work. To test our method, we implemented a tool, Cable, for debugging specifications. We have used Cable to debug specifications produced by Strauss, our specification miner. We found that using Cable to debug these specifications requires, on average, less than one third as many user decisions as debugging by examining all traces requires. In one case, using Cable required only 28 decisions, while debugging by examining all traces required 224.

Electronic downloads

Citation formats  
  • HTML
    Glenn Ammons, David Mandelin, Rastislav Bodik, James Larus.
    <a
    href="http://chess.eecs.berkeley.edu/pubs/756.html"
    >Debugging Temporal Specifications with Concept
    Analysis</a>, Proceedings of the ACM SIGPLAN 2003
    conference on Programming language design and
    implementation, June, 2003.
  • Plain text
    Glenn Ammons, David Mandelin, Rastislav Bodik, James Larus.
    "Debugging Temporal Specifications with Concept
    Analysis". Proceedings of the ACM SIGPLAN 2003
    conference on Programming language design and
    implementation, June, 2003.
  • BibTeX
    @inproceedings{AmmonsMandelinBodikLarus03_DebuggingTemporalSpecificationsWithConceptAnalysis,
        author = {Glenn Ammons and David Mandelin and Rastislav
                  Bodik and James Larus},
        title = {Debugging Temporal Specifications with Concept
                  Analysis},
        booktitle = {Proceedings of the ACM SIGPLAN 2003 conference on
                  Programming language design and implementation},
        month = {June},
        year = {2003},
        abstract = {Program verification tools (such as model checkers
                  and static analyzers) can find many errors in
                  programs. These tools need formal specifications
                  of correct program behavior, but writing a correct
                  specification is difficult, just as writing a
                  correct program is difficult. Thus, just as we
                  need methods for debugging programs, we need
                  methods for debugging specifications. This paper
                  describes a novel method for debugging formal,
                  temporal specifications. Our method exploits the
                  short program execution traces that program
                  verification tools generate from specification
                  violations and that specification miners extract
                  from programs. Manually examining these traces is
                  a straightforward way to debug a specification,
                  but this method is tedious and error-prone because
                  there may be hundreds or thousands of traces to
                  inspect. Our method uses concept analysis to
                  automatically group the traces into highly similar
                  clusters. By examining clusters instead of
                  individual traces, a person can debug a
                  specification with less work. To test our method,
                  we implemented a tool, Cable, for debugging
                  specifications. We have used Cable to debug
                  specifications produced by Strauss, our
                  specification miner. We found that using Cable to
                  debug these specifications requires, on average,
                  less than one third as many user decisions as
                  debugging by examining all traces requires. In one
                  case, using Cable required only 28 decisions,
                  while debugging by examining all traces required
                  224.},
        URL = {http://chess.eecs.berkeley.edu/pubs/756.html}
    }
    

Posted by Christopher Brooks on 4 Nov 2010.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess