Assertional Reasoning for Concurrent and Communicating BPEL-like Programs
Journal Title: Annals of Computer Science and Information Systems - Year 2018, Vol 17, Issue
Abstract
This paper studies verification of programs similar to BPEL4WS (BPEL), the latter being a de facto standard for the web services composition and orchestration. Traditionally, in verification of concurrent and distributed programs, the model was either based on shared variables or message passing and was studied separately. BPEL-like programs have features that are present in both models: several flows within one service can be executed in parallel and they can access shared variables, whereas several services communicate by message passing. Therefore, it is natural that for verification of BPEL-like programs, the verification methods developed for shared variables and message passing be integrated. In this paper, we combine the proof rules for shared variable programs from Owicki and Gries, the proof rules for CSP like programs from Apt, Francez and de Roever, together with proof rules for compensation and fault handling, to cover all major features of BPEL. An operational semantics is presented and the proof rules can be justified over that. Examples are provided to show the feasibility of verification framework.
Authors and Affiliations
Longfei Zhu, Qiwen Xu, Huibiao Zhu
Keywords
Related Articles
- EP ID EP567972
- DOI 10.15439/2018F148
- Views 32
- Downloads 0
An Adaptive Approach Digital Image Watermarking based on Discrete Wavelet Transform (DWT)
The applications of different dimension of multimedia have been grown rapidly on daily basis. Digital media brings about the changes in the conveniences to the people, The cons of this technology is security threat if th...
The Practical Use of Problem Encoding Allowing Cheap Fitness Computation of Mutated Individuals
The usual assumption in the Evolutionary Computation field is that a cost of computing single fitness function evaluation is at last similar for all cases. Such assumption does not have to be true. In this paper we consi...
Soccer object motion recognition based on 3D convolutional neural networks
Due to the development of video understanding and big data analysis research field using deep learning technique, intelligent machines have replaced the tasks that people performed in the past in various fields such as t...
Kestrel-based Search Algorithm (KSA) and Long Short Term Memory (LSTM) Network for feature selection in classification of high-dimensional bioinformatics datasets
Although deep learning methods have been applied to the selection of features in the classification problem, current methods of learning parameters to be used in the classification approach can vary in accuracy at each t...
Optimizing Maintenance in Project Management by Considering HSE and Resilience Engineering
One of the most important objectives of project management is to complete the project within the specified completion date of the project. Another important objective of project is to terminate the project by minimum rat...