Introducing Specification-Based Data Structure Repair Using Alloy

Razieh Nokhbeh Zaeem, Sarfraz Khurshid
Digital Printed Abstract View Cite
Type
Short Paper
Publication
2nd International Conference on ASM, Alloy, B, and Z (ABZ'10)

Abstract

While several different techniques utilize specifications to check correctness of programs before they are deployed, the use of specifications in deployed software is more limited, largely taking the form of runtime checking where assertions form a basis for detecting erroneous program states and terminating erroneous executions in failures. Recent approaches [1] proposed constraint-based repair where data structure constraints are used to repair erroneous states. However, data structure constraints are too weak a form of specification for error recovery in general. We have developed a specification-based approach for data structure repair, which allows repairing erroneous executions in deployed software by repairing erroneous states. The key novelty is our support for rich behavioral specifications, such as those that relate pre-states with post-states to accurately specify expected behavior and hence to enable precise repair.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{ZaeemK10,
  author       = {Razieh Nokhbeh Zaeem and
                  Sarfraz Khurshid},
  editor       = {Marc Frappier and
                  Uwe Gl{\"{a}}sser and
                  Sarfraz Khurshid and
                  R{\'{e}}gine Laleau and
                  Steve Reeves},
  title        = {Introducing Specification-Based Data Structure Repair Using Alloy},
  booktitle    = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
                  {ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5977},
  pages        = {398--399},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-11811-1\_34},
  doi          = {10.1007/978-3-642-11811-1\_34},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/ZaeemK10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'10

Related