icon-carat-right menu search cmu-wordmark

Assume-Guarantee Reasoning for Deadlock

Technical Note
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
DOI (Digital Object Identifier)
10.1184/R1/6572054.v1

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.

Cite This Technical Note

Chaki, S., & Sinha, N. (2006, September 1). Assume-Guarantee Reasoning for Deadlock. (Technical Note CMU/SEI-2006-TN-028). Retrieved November 9, 2024, from https://doi.org/10.1184/R1/6572054.v1.

@techreport{chaki_2006,
author={Chaki, Sagar and Sinha, Nishant},
title={Assume-Guarantee Reasoning for Deadlock},
month={{Sep},
year={{2006},
number={{CMU/SEI-2006-TN-028},
howpublished={Carnegie Mellon University, Software Engineering Institute's Digital Library},
url={https://doi.org/10.1184/R1/6572054.v1},
note={Accessed: 2024-Nov-9}
}

Chaki, Sagar, and Nishant Sinha. "Assume-Guarantee Reasoning for Deadlock." (CMU/SEI-2006-TN-028). Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, September 1, 2006. https://doi.org/10.1184/R1/6572054.v1.

S. Chaki, and N. Sinha, "Assume-Guarantee Reasoning for Deadlock," Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, Technical Note CMU/SEI-2006-TN-028, 1-Sep-2006 [Online]. Available: https://doi.org/10.1184/R1/6572054.v1. [Accessed: 9-Nov-2024].

Chaki, Sagar, and Nishant Sinha. "Assume-Guarantee Reasoning for Deadlock." (Technical Note CMU/SEI-2006-TN-028). Carnegie Mellon University, Software Engineering Institute's Digital Library, Software Engineering Institute, 1 Sep. 2006. https://doi.org/10.1184/R1/6572054.v1. Accessed 9 Nov. 2024.

Chaki, Sagar; & Sinha, Nishant. Assume-Guarantee Reasoning for Deadlock. CMU/SEI-2006-TN-028. Software Engineering Institute. 2006. https://doi.org/10.1184/R1/6572054.v1