Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

Technical Note

Assume-Guarantee Reasoning for Deadlock

  • September 2006
  • By Sagar Chaki, Nishant Sinha
  • This report shows how L^F can be used for compositional regular failure language containment and deadlock detection, using non-circular and circular assume-guarantee rules.
  • Publisher: Software Engineering Institute
    CMU/SEI Report Number: CMU/SEI-2006-TN-028
  • Abstract

    The use of learning to automate assume-guarantee style reasoning has received a lot of attention in recent years. This paradigm has already been used successfully for checking trace containment, as well as simulation between concurrent systems and their specifications. In this report, the learning-based automated assume-guarantee paradigm is extended to perform compositional deadlock detection. Failure automata is defined as a generalization of finite automata that accept regular failure sets. A learning algorithm LF is developed that constructs the minimal deterministic failure automata accepting any unknown regular failure set using a minimally adequate teacher. This report shows how LF can be used for compositional regular failure language containment and deadlock detection, using non-circular and circular assume-guarantee rules. Finally, an implementation of techniques and encouraging experimental results on several nontrivial benchmarks are presented.

  • Download

Cite This Report

SEI

Chaki, Sagar; & Sinha, Nishant. Assume-Guarantee Reasoning for Deadlock. CMU/SEI-2006-TN-028. Software Engineering Institute, Carnegie Mellon University. 2006. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7957

IEEE

Chaki. Sagar, and Sinha. Nishant, "Assume-Guarantee Reasoning for Deadlock," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Note CMU/SEI-2006-TN-028, 2006. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7957

APA

Chaki, Sagar., & Sinha, Nishant. (2006). Assume-Guarantee Reasoning for Deadlock (CMU/SEI-2006-TN-028). Retrieved March 22, 2017, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7957

CHI

Sagar Chaki, & Nishant Sinha. Assume-Guarantee Reasoning for Deadlock (CMU/SEI-2006-TN-028). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2006. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7957

MLA

Chaki, Sagar., & Sinha, Nishant. 2006. Assume-Guarantee Reasoning for Deadlock (Technical Report CMU/SEI-2006-TN-028). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7957

BibTex

@techreport{ChakiAssumeGuaranteeReasoning2006,
title={Assume-Guarantee Reasoning for Deadlock},
author={Sagar Chaki and Nishant Sinha},
year={2006},
number={CMU/SEI-2006-TN-028},
institution={Software Engineering Institute, Carnegie Mellon University},
address={Pittsburgh, PA},
url={http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7957} }