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 36
- Downloads 0
Detection of Malicious Executables Using Rule Based Classification Algorithms
Machine Learning class rule has varied packages together with classification, clustering, will understand association rules furthermore and is capable of the method an enormous set of the information set as measure super...
Acoustic Model Training, using Kaldi, for Automatic Whispery Speech Recognition
The article presents research on the automatic whispery speech recognition. The main task was to find dependences between a number of triphone classes (number of leaves in decision tree) and the total number of Gaussian...
Importance of Text Data Preprocessing & Implementation in RapidMiner
Data preparation is an important phase before applying any machine learning algorithms. Same with the text data before applying any machine learning algorithm on text data, it requires data preparation. The data preparat...
Simulation Driven Development of Distributed Systems – Coupling of virtual and real system components
Looking at the end-to-end processing, typical software-intensive systems are built as a system-of-systems where each sub-system specializes according to both the business and technology perspective. One challenge is the...
A Perspective Approach (OABC) Algorithm using Square Odd Routing for minimized Energy Consumption
ABC set of principles has been already proposed furthermore with some drove guidelines, yet the length of the work parameter has been spinning round detecting the hubs in static or dynamic way with no accentuation at the...