Formal Depiction of Composition of Web Services Based on CCS and Modal Mu-Calculus

How to guarantee the validity of Web services composition is one of the study hot topics in theory and practice. An important research field is to describe and characterize Web services by formal method which is an effective way for modeling concurrent systems. In this paper, we formalize Web services composition using CCS, a classical process algebra, and display which is an effective way through a case study. Furthermore we utilize interrelated modal-calculus which is a appropriate program logic for characterizing properties of the formal model established by using CCS. Some properties is discussed such as capacity, necessity, safety and liveness.