Title: Validating trustworthy service composition through VIPLE and pi-calculus

Authors: Shenghui Zhao; Yuemin Li; Yang Wang; Yinong Chen

Addresses: College of Computer Information and Engineering, Chuzhou University, Chuzhou, Anhui, China ' College of Computer Information and Engineering, Chuzhou University, Chuzhou, Anhui, China ' College of Computer Information and Engineering, Chuzhou University, Chuzhou, Anhui, China ' School of Computing, Informatics and Decision System Engineering, Arizona State University, Tempe, AZ 85287, USA

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.

Keywords: formal verification; pi-calculus; service composition; visual programming; VIPLE.

DOI: 10.1504/IJSPM.2020.106971

International Journal of Simulation and Process Modelling, 2020 Vol.15 No.1/2, pp.76 - 88

Received: 06 Sep 2018
Accepted: 04 Apr 2019
Published online: 29 Apr 2020 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article