%0 Conference Proceedings %T Lending Petri Nets and Contracts %+ Dipartimento di Matematica e Informatica %A Bartoletti, Massimo %A Cimoli, Tiziana %A Pinna, G., Michele %< avec comité de lecture %( Lecture Notes in Computer Science %B 5th International Conference on Fundamentals of Software Engineering (FSEN) %C Tehran, Iran %Y Farhad Arbab %Y Marjan Sirjani %I Springer Berlin Heidelberg %3 Fundamentals of Software Engineering %V LNCS-8161 %P 66-82 %8 2013-04-24 %D 2013 %R 10.1007/978-3-642-40213-5_5 %Z Computer Science [cs]Conference papers %X 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 an 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. %G English %2 https://inria.hal.science/hal-01514665/document %2 https://inria.hal.science/hal-01514665/file/978-3-642-40213-5_5_Chapter.pdf %L hal-01514665 %U https://inria.hal.science/hal-01514665 %~ IFIP-LNCS %~ IFIP %~ IFIP-TC %~ IFIP-TC2 %~ IFIP-WG2-2 %~ IFIP-FSEN %~ IFIP-LNCS-8161