一种能够描述可信特征的进程代数  

QPi:A Calculus to Enforce Trustworthiness Requirements

作　　者：符宁[1,2] 周兴社[1] 詹涛[1] 

机构地区：[1]西北工业大学计算机学院,西安710072 [2]解放军西安政治学院,西安710068

出　　处：《计算机研究与发展》2011年第11期2120-2130,共11页Journal of Computer Research and Development

基　　金：国家"八六三"高技术研究发展计划重大专项基金项目(2009AA010308);国家"八六三"高技术研究发展计划基金项目(2006AA01Z162);国家发展与改革委员会基金项目(20052139);国家"十一五"国防预研基金项目(06004089)

摘　　要：针对可信服务计算需要对系统行为和可信特征进行建模和分析的要求,结合具有描述多个维度可信特征能力的Q代数对Pi演算进行扩展,提出一种可用于对系统行为及可信特征进行建模的进程代数,称之为QPi.QPi将可信特征附加于进程动作,在描述系统行为的同时体现出其可信特征.进一步引入互相似距离的概念以考察2个进程在多大程度上是能够互相模拟的,并研究了QPi与之相关的若干性质.具体的实例描述说明了该代数方法的有效性.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 hisimulation distance. QPi related properties of bisimulation and bisimilarity are also discussed. Demonstrative examples reveal the effectiveness of the calculus.

关 键 词：可信软件 进程代数 PI演算 Q代数 半环 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]