Lending Petri nets and contracts

TL;DR

This paper introduces a Petri net-based model for service contracts that enables services to safeguard themselves within choreographies, linking it with Propositional Contract Logic for verification.

Contribution

It extends Petri nets to incorporate contracts, providing a formal framework for secure service composition and a translation to logic for verification.

Findings

Model preserves logical agreement in service contracts.

Enables compositional verification of service interactions.

Bridges Petri nets with Propositional Contract Logic.

Abstract

Choreography-based approaches to service composition typically assume that, after a set of services has been found which correctly play the roles prescribed by the choreography, each service respects his role. Honest services are not protected against adversaries. We propose a model for contracts based on a extension of Petri nets, which allows services to protect themselves while still realizing the choreography. We relate this model with Propositional Contract Logic, by showing a translation of formulae into our Petri nets which preserves the logical notion of agreement, and allows for compositional verification.