Paper Info
Title
Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams
Abstract
The explosion in the number of states due to several interacting components limits the application of model checking in practice. Compositional reasoning ameliorates this problem by reducing reasoning about the entire system to reasoning about individual components. Such reasoning is often carried out in the assume-guarantee paradigm: each component guarantees certain properties based on assumptions about the other components. Na茂ve applications of this reasoning can be circular and, therefore, unsound. We present a new rule for assume-guarantee reasoning, which is sound and complete. We show how to apply it, in a fully automated manner, to properties specified as synchronous timing diagrams. We show that timing diagram properties have a natural decomposition into assume-guarantee pairs, and liveness restrictions that result in simple subgoals which can be checked efficiently. We have implemented our method in a timing diagram analysis tool, which carries out the compositional proof in a fully automated manner. Initial applications of this method have yielded promising results, showing substantial reductions in the space requirements for model checking.
Year
DOI
Venue
2001
10.1007/3-540-45319-9_32
TACAS
Keywords
Field
DocType
synchronous timing diagrams,assume-guarantee pair,assume-guarantee reasoning,compositional reasoning,model checking,automated manner,certain property,timing diagram analysis tool,assume-guarantee paradigm,synchronous timing diagram,timing diagram property
Timing diagram,Model checking,Concurrency,Computer science,Expert system,Algorithm,Theoretical computer science,Diagram,Reasoning system,Memory controller,Liveness
Conference
ISBN
Citations 
PageRank 
3-540-41865-2
20
0.97
References 
Authors
8
4
Name
Order
Citations
PageRank
Nina Amla131816.23
e allen emerson276831183.13
Kedar S. Namjoshi394850.41
Richard J. Trefler422214.59