In this survey, we overview several compositional verification approaches based on model checking, namely compositional minimization, classic assume guarantee reasoning and circular reasoning. We describe details of each of these approaches, and elaborate the general problems with some proposed solutions. We also summarize the advantages and disadvantages of each. In the last section, we give a general conclusion for future directions of compositional verification. Through the analysis, we discuss how the notions of preorder and abstraction play an important role in the reasoning. Finally, we will see some new trends in the development of compositional verification methodologies, e.g., the integration of theorem proving and model checking approaches in the compositional reasoning context.

Download postscript file (PS File)

Send comments and suggestions to: pengh@ece.concordia.ca