Efficient Verification of Service-Based Applications for Flexible Modeling
Min Yuan, Zhiqiu Huang · 2018
Formal verification has been shown to be a useful technique for performing assurance of electronic business transactions. However the verification efficiency is still a serious bottleneck due to increasingly complex system deployed over multiple data centers. Although great improvements in the state-of-the-art model-checking algorithms, the optimization on the business process level has an advantage in improving verification performance. From a transactional equivalence perspective a method to minimize the target business transactions model and improve the verification efficiency is presented. This work proposes a formal modeling method for a flexible transaction based on an extension of Pi-calculus. An operational semantics is defined as an extension of the classical one for Pi-calculus by introducing membrane activities (a kind of wrapper for processes). Then, a weak bisimulation relation is defined, which is used to reduce the transaction models and apply checking transactions equivalence. A running example throughout the entire paper empirically evaluates the performance of the proposed solutions. The experimental results show a significant improvement in terms of state space and construction time. This will make it possible to provide improvements in the performance efficiency for verifying Service-based applications.