Affiliations: [a] Polytechnic School of Montreal, Montréal, QC, Canada | [b] Newcastle University, Newcastle upon Tyne, UK | [c] UNU-IIST, Macao, China
Correspondence:
[*]
Corresponding author: F. Abouzaid, Polytechnic School of Montreal, Montréal, QC, Canada. E-mail: m.abouzaid@polymtl.ca
Abstract: The BP-calculus is a formalism based on the π-calculus, which is encoded in WS-BPEL. The BP-calculus is intended to specifically model and verify Service Oriented Applications (SOA). One important feature of SOA is the ability to compose services which may evolve dynamically or at runtime. Dynamic reconfiguration of services increases their availability but, simultaneously, it complicates validation, verification, and evaluation to some extent. In this paper, we formally model and analyze dynamic reconfigurations and their requirements in BP-calculus and we show how reconfigurable components can be modeled using handlers that are essential parts of WS-BPEL language. Besides, we consider security rules and their formal specification as required to implement dynamic reconfiguration.
