Lending Petri nets and contracts

Post date: 17-Dec-2012 09:17:51

Upcoming paper (to be presented at FSEN 2013, Tehran, Apr 24-26 2013)

Lending Petri nets and contracts

M. Bartoletti, T. Cimoli and G.M. Pinna

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.

References.

M. Bartoletti, T. Cimoli and G.M. Pinna. Lending Petri nets and contracts. CoRR abs/1211.3624. To appear in Proc. FSEN 2013.