{'fraction_non_alphanumeric': 0.017823639774859287, 'fraction_numerical': 0.001876172607879925, 'mean_word_length': 5.0625, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Toward a Pi-Calculus Based Verification Tool for Web Services Orchestrations

Web services constitute a dynamic field of research about technologies of the Internet. WS-BPEL 2.0, is in the way for becoming a standard for defining Web services orchestration. To check the good behaviour of the produced compositions, but also to check equivalence between services, formalization is necessary. In this paper a contribution to the field of Formal Verification of Web services composition is presented using a πcalculus-based approach for the verification of composite Web services by applying model checking methods. We adopt the possibility of exploiting benefits from existing works by translating a Business Process Language such as BPEL to a system model of the π-calculus for which analysis and verification techniques have already been well established and there are existing tools for model checking systems. We therefore present the basis of a framework aimed to specification and verification, related to some temporal logic, of Web services composition. . . .