In the compositional verification of a concurrent system, one seeks to deduce properties of the system from properties of its constituent modules. This paper supplements our previous work on the same subject to provide a comprehensive compositional framework in linear-time temporal logic. It has been shown by many that specifying properties of a module in the assumption-guarantee style is effective in achieving compositionality. We consider two forms of temporal formulas that correspond to two interpretations of an assumption-guarantee specification and investigate how they can be applied in compositional verification. We argue by examples that the two forms complement each other and both are needed to facilitate the compositional approach. We also show how to handle assumption-guarantee specifications where the assumption contains a liveness property.
展开▼
