A K-BPEL Semantics
Khadhir Bekki, Hafida Belbachir, Wafaa Kasri · 2015
In the last years, various works of checking the modeling of business process are proposed. But, Most of them are based on the models transformation, to transform the model captured (to another model (eg Petri Net) to check. Therefore, It may affect the transformed semantic quality, thus on verification. The framework K is a tool based on rewriting logic and Maude. It is a system for formally defining programming languages. It is shown how sequential or concurrent languages can be defined in K simply and modularly. It offers many services which assess easily experiment with language design by means of testing and behavior exploration with a unique formal model. In this work, our contribution is to describe a formal semantic of a business process execution language (BPEL) using the framework K.