QPi: A Calculus to Enforce Trustworthiness Requirements

As service becomes the core concept for the abstraction and wrapping of diverse resources in open environment, a new software development paradigm which constructs applications based on services and service compositions becomes the mainstream technology and the direction of distributed computing. With the related researches and applications developing in depth, more and more people have realized that we must pay more attention to trustworthiness under the precondition of functional implementation when constructing service application in open, dynamic computing environment. Software theories and formal methods are regarded as the key for assuring the correctness and trustworthiness of software. Trustworthy computing requires the theories for modeling and analyzing business process in terms of both behavior and trustworthiness. A calculus for assuring satisfaction of trustworthiness requirements in service-oriented systems is proposed in this paper. We investigate a calculus called QPi, for representing both behavior and trustworthiness property of processes. QPi is the combination of Pi calculus and constraint semi-ring, which has a unique advantage when problems with multiple trustworthiness dimensions must be tackled. The notion of quantified bisimulation on process provides us a measure on the degree of equivalence of process based on bisimulation distance. QPi related properties of bisimulation and bisimilarity are also discussed. Demonstrative examples reveal the effectiveness of the calculus.