Validating trustworthy service composition through VIPLE and pi-calculus. (21st April 2020)

• Record Type: Journal Article
• Authors: Zhao, Shenghui; Li, Yuemin; Wang, Yang; Chen, Yinong
• Is Part Of: International journal of simulation and process modelling. Volume 15:Number 1/2(2020)
• Page Start: 76
• Page End: 88
• Publication Date: 2020-04-21
• Subjects: formal verification -- pi-calculus -- service composition -- visual programming -- VIPLE; Management -- Computer simulation -- Periodicals; Mathematical models -- Periodicals; Operations research -- Periodicals; Simulation methods -- Periodicals; 003.05
• Languages: English
• ISSNs: 1740-2123

Abstract

The current formal verification practice focuses on functionality and does not consider verification of the non-functional attributes. In this study, we propose a method in which non-functional attributes are incorporated into the logic rules of inference in terms of composition of the linear logic and pi-calculus. Giving the credibility to non-functional attributes is important, especially in the cloud computing platform and IoT environments, where trust and security are ultra-important. Such studies have not been paid much attention by researchers and practitioners. In our approach, the evolvement of the non-functional attributes is included in the process of formal verification of the service composition scheme. In addition to theoretical analysis, we applied a tool named Visual IoT/robotics Programming Language Environment (VIPLE) to execute and verify the validity of the service composition model's function. We translate the proving process of the linear logic into the corresponding pi-calculus expressions. VIPLE can translate visual work flow into pi-calculus and can verify the correctness of pi-calculus expressions.