Verifiable abstractions for contract-oriented systems ?
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.
verification contract-oriented computing rewriting logic session types