On The Verification Of Trusted And Autonomic Service Cooperation Systems

The XML standards and service-oriented computing(SOC) paradigm greatly reduced the difficulty and cost of implementing Cross Organizational Cooperation(COC) systems such as Multi-Agent Cooperation System(MACS),Virtual Organization(VO) and E-Institution,etc.,thus make the widely application of such systems a reality.But the complexity of these models,the distribution of component and the asynchronism of component execution hampered the the verification of such models.How to verify whether the implemented system can satisfy the desired property,whether it is consistent and complete is one of the main challenges during the process of system design and implementation.At present,test and formal verification is the main approach for system verification. By contrast,the traditional testing technologies cannot meet the requirements because it can not guarantee to cover all execution paths.Because of its strictness,accuracy and automation,the automated formal verification theories and technologies based on formal methods is the best choice for COC system verification.Because of the architectural difference,we can not propose a general solution for COC system verification.But the research on typical system verification can provide valuable insights for others to reduce the cost.The Trusted and Autonomic Service Cooperation System(TASCS) is a new kind of trusted COC platform under the SOC paradigm.It encompasses the main principles and technologies of the mainstream COC systems,so the research on TASCS verification is valuable for other systems.Based on our research on cross organizational service cooperation and automated formal verification,this thesis introduced an automated verification solution for TASCS,thus gave a demonstration for the verification of other COC models.The main content of this thesis can be described as follows:In the thesis,we first introduced the two main automated formal verification methods—model checking and decision procedure.We presented the basic concepts, theories,technologies and the principal tools,analyzed their applicability and constraints.Secondly,we introduced the two main theoretical basis of TASCS-the ebXML distributed cooperation model and the Norm-governed Multi-agent Cooperation System(NMCS) model,among them the former is the reference model of TASCS Distributed Business Process and the latter is the theoretical base of TASCS trust mechanism.We presented a NMCS dynamic model and a property verification mechanism for this model.Because the TASCS model is in essence a special case of the NMCS model,so the mechanism provided the main inspiration for the TASCS dynamic property verification method.Next,we presented a system dynamic property verification solution for TASCS model which is based on symbolic model checking.In this solution we designed a propositional deontic logic based formal normative language and its state-set semantic, and seamlessly embedded it into the Kripke structure,thus bridged the semantic gap between norm and system model.The symbolic model checking algorithms designed on top of this can effectively verify the dynamic properties of the TASCS model.Next,we analyzed the consistency problems of DBPs arose during the designing and implementing processes of the TASCS model and classified them into several categories.We presented an DBP consistency verification solution based on decision procedure technologies for formal sentences.This solution first modeled the consistency problems with propositional logic and Equality logic with Uninterpreted Functions(EUF) sentences,and then translated them into the equivalent propositional normal forms,and verified them with the corresponding decision procedures.This solution can effectively model and verify the main DBP consistency problems.Finally,we introduced the architecture of organ/tissue transplantation COC system, presented the application of our verification solutions in this system,and discussed their virtues and weaknesses,and their value for the verification of other COC models.