Lending Petri Nets and Contracts
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 adv
- PDF / 456,296 Bytes
- 17 Pages / 439.37 x 666.142 pts Page_size
- 53 Downloads / 265 Views
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 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.
1
Introduction
Many of today’s human activities, from business and financial transactions, to collaborative and social applications, run over complex interorganizational systems, based on service-oriented computing (SOC) and cloud computing technologies. These technologies foster the implementation of complex software systems through the composition of basic building blocks, called services. Ensuring reliable coordination of such components is fundamental to avoid critical, possibly irreparable problems, ranging from economic losses in case of commercial activities, to risks for human life in case of safety-critical applications. Ideally, in the SOC paradigm an application is constructed by dynamically discovering and composing services published by different organizations. Services have to cooperate to achieve the overall goals, while at the same time they have to compete to achieve the specific goals of their stakeholders. These goals may be conflicting, especially in case of mutually distrusted organizations. Thus, services must play a double role: while cooperating together, they have to protect themselves against other service’s misbehavior (either unintentional or malicious). The lack of precise guarantees about the reliability and security of services is a main deterrent for industries wishing to move their applications and business to the cloud [3]. Quoting from [3], “absent radical improvements in security technology, we expect that users will use contracts and courts, rather than clever security engineering, to guard against provider malfeasance”. Indeed, contracts are already a key ingredient in the design of SOC applications. A choreography is a specification of the overall behavior of an interorganizational process. This global view of the behavior is projected into a set of local views, which specify the behavior expected from each service involved in the whole process. The local views can be interpreted as the service contracts: if F. Arbab and M. Sirjani (Eds.): FSEN 2013, LNCS 8161, pp. 66–82, 2013. DOI: 10.1007/978-3-642-40213-5 5, c IFIP International Federation for Information Processing 2013
Lending Petri Nets and Contracts
67
the actual implementation of each service respects its contract, then the overall application must be guaranteed to behave correctly. There are many proposals of formal models for contracts in the literature, which we may roughly divide into “phy
Data Loading...
