关键词：关联接口；担保合同；关系理论；规范化
摘 要：Contract-based design is emerging as a unifying compositional paradigm for the speci cation, design and veri cation of large-scale complex systems. Yet, di erent contract frameworks are currently available, without a clear understanding of the relations between them. In this paper, we investigate the relation between interface theories (specifically, relational interfaces) and assume-guarantee (A/G) contracts, revealing some of the subtleties involved. We show that the natural transformation of interfaces to A/G contracts represented by LTL formulas preserves re nement,but does not generally preserve serial composition, and we present an assumption-projection operator to remedy the latter issue. We also discuss the properties of our transformation with respect to conjunction. Finally, we provide illustrative examples that shed light on the e ectiveness of both frameworks for requirement formalization, early detection of integration errors, and principled use of abstraction renement.
内 容：