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 55
- Downloads 0
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...
Data quality evaluation: a comparative analysis of company registers’ open data in four European countries
This paper is devoted to the analysis of open data quality of the company registers in four different countries. The data quality evaluation was obtained using a methodology that involves the creation of three-part data...
Financial Inclusion in India and PMJDY: A Critical Review
The recent developments in banking and insurance have transformed the financial system, however, it is restricted only to certain segments of the society, excluding others. i.e. ``financial exclusion''. People with low i...
Proposal for simplified implementation of risk assessment method for measuring instruments
Legal Metrology is the economic sector where measuring instruments subject to legal control (taximeters, electricity meters, etc.) are used. In this field, constant growth of Measuring Instruments using ICT technology is...
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...