Verifiable abstractions for contract-oriented systems

详细信息    查看全文

• 作者：Massimo Bartoletti^a ; ^{bart@unica.it} ; Maurizio Murgia^a ; Alceste Scalas^a ; Roberto Zunino^b
• 关键词：Contract-oriented computing ; Verification ; Rewriting logic ; Session types
• 刊名：Journal of Logical and Algebraic Methods in Programming
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：86
• 期：1
• 页码：159-207
• 全文大小：1139 K
• 卷排序：86

文摘

We present a specification language for distributed systems where the interaction between agents is regulated by contracts. We consider the honesty property, which characterises those agents which always respect their contracts. We propose a sound verification technique for honesty, based on semantic abstraction and model checking. We describe a Maude implementation of our verification technique. We provide detailed proofs of all our statements, and a suite of experiments to validate our technique.