Web Services and Formal Methods (WS-FM 2013)

• About
• Call for Papers
• Past Events
• Committees
• Programme and Registration
• Venue and Accommodation

Registration

Programme

Keynotes

Invited Speakers

• Dr. Weicheng Huang, National Center for High-Performance Computing, Taiwan
Title: Introducing Cloud Activities Around Pacific Rim

Abstract Following footsteps of the Parallel Computing and the Grid Computing, the Cloud Computing has become the world noticed advanced computing technology. The key elements that put the Cloud into the spot light are 1) virtualization, 2) extremely large scale, 3) high availability, 4) high reliability, 5) high scalability, 6) low cost, 7) pay-as-you-go etc. In the past few years, even though it has passed the highest visibility point in Hype Cycle of Technology, this new face of computing technology still keep its momentum and is considered as major paradigm shift of the computing technology. The Cloud market has encouraged all the vendors, domestically and internationally alike, to devote themselves into the three tiers of the Cloud Computing, namely, Infrastructure-as-a-Service (IaaS), Platform-as-a-Service (PaaS), and Software-as-a-Service (SaaS).
Unavoidably, the Multi-tenancy is the present and future Cloud environment presented to the users. Although various technological issues have to be solved, for example, unified fabric which is crucial to the connectivity within and outside of the Data Center to keep the data flow smoothly, the unified computing mechanism that keeps the computing transparent to the users, ... etc. The vision of accessing Cloud Computing the way we access the water and electricity in our daily live is still to be accomplished.
In this presentation, we will not attempt to deliver answers to all the existing technological questions. Instead, the international efforts around the Pacific Rim area will be introduced with important development issues exposed. For example, with joint efforts of multiple participants from different organization/entities, the effort of dealing with the Cloud Interoperability issue is under investigation in order to break the possible lock-in problem of the Cloud. The efforts to lower the barrier and cost of VM image translate between different Cloud environments and thus to speed up the popularity of the Cloud will also be touched. The purpose of the discussion of these efforts is not to deliver a full solution to the Cloud environment, but to shade light on the future development of Cloud technology.

• Prof. Jianwen Su, Department of Computer Science, U C Santa Barbara
Title: Choreography Revisited

Abstract A business process (BP) is an assembly of work activities (automated or by human performers) to accomplish a business goal. A collaborative business process (CBP) coordinates participating BPs in order to achieve a complex business objective. A CBP may employ a "mediator" to ensure its business logic to be carried out faithfully; such a "hub-and-spoke" approach is widely used in practice, e.g., through the use of BPEL. The mediator is often an apparent bottleneck in many aspects. As an alternative, a participating BP in a "peer-to-peer" CBP communicates only with its partners based on needs and there is possibly no single participant BP that is aware of global progress during execution. A "choreography" models a class of similar peer-to-peer CBPs. While this is more desired, existing choreography languages (1) are weak in modeling data shared by participants and used in message sequence constraints and (2) assume a fixed number of participants and make no distinction between participant types and participant instances.
In this talk, we argue that the traditional concept of a choreography needs to be augmented to support data and participant instances. We present a new declarative language based on the widely known artifact-centric BP modeling approach. Our language has four ingredients: (1) Each participant type is an artifact schema with its information model partially visible to choreography specification. (2) Participant instance correlations are supported explicitly and cardinality constraints on such correlations can be defined. (3) Messages have data contents to be used in choreography constraints. (4) The language is declarative based on first-order and linear time (LTL) logics. In particular, Skolem notations are used to represent dependencies in a succinct manner. We will also discuss some technical results concerning the properties of this language.

Schedule

Thursday, 29 August 2013

Friday, 30 August 2013