Validating trustworthy service composition through VIPLE and pi-calculus

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.