Specification and Analysis of Service Oriented Architectures within the Calculus of Communicating Sequential Processes (CSP)

摘要

Software architecture evolved from the monolithic paradigm to the Service-Oriented Computing (SOC) paradigm. IT systems in the SOC paradigm are based on service compositions. A service composition is an aggregate of loosely coupled autonomous heterogeneous services which are collectively composed to implement a particular task. Internet standards are the dominant modelling methods of SOC systems. How- ever, they raise fundamental issues: standards lack formalism, and they fall short when being applied independently. The former issue has been solved and rigorous semantics have been developed for the di erent standards. However, the latter is- sue has only partially been solved, by developing new formal modelling languages that are adopting the concepts rather than the notations of the internet standards. In principle, the main concepts that should be hosted in SOC modelling languages are: asynchronicity, mobility, multiparty sessions, and compensations. However, not all of these concepts are supported in the current developed modelling languages. This thesis addresses this problem and proposes a new formal modelling language for SOC systems which is adequately expressive to model the previous concepts. Additionally, the thesis provides an implementation for the new modelling language in a model checker to facilitate automated formal reasoning on systems properties like: good/bad traces, deadlock-freedom, and livelock-freedom.