Are interface theories equivalent to contract theories?
Formal Methods and Models for Codesign(2014)
摘要
Contract-based design is emerging as a unifying compositional paradigm for the specification, design and verification of large-scale complex systems. Different contract frameworks are currently available, but we lack 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. We introduce a natural transformation of interfaces to A/G contracts represented by linear temporal logic. Then, we analyze differences and correspondences between key operators and relations in the two theories (i.e. composition, refinement and conjunction), by studying their preservation properties under the proposed transformation. We show that the transformation preserves refinement, but does not generally preserve serial composition and conjunction. Then, we present an assumption-projection operator to make it possible to preserve serial composition and compatibility checking. Finally, we provide illustrative examples that shed light on the effectiveness of both frameworks for requirement formalization, early detection of integration errors, and use of abstraction-refinement.
更多查看译文
关键词
contracts,formal specification,formal verification,large-scale systems,temporal logic,a/g contracts,assume-guarantee contracts,assumption-projection operator,contract theories,contract-based design,early integration error detection,interface theories,large-scale complex system design,large-scale complex system specification,large-scale complex system verification,linear temporal logic,relational interface,requirement formalization,serial composition,serial conjunction,unifying compositional paradigm,automata,law,mathematical model,cost accounting
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络