FORMAL MODEL DEFINITION OF WEB SERVICE BEHAVIOR FROM SOURCE CODE IN REWRITE LOGIC

Abstract

Developers of web applications strive for implementing state-of-the-art design patterns. One of them is microservice architecture design, which increases the number of web services employed in the applications’ back end. Formal verification may help to verify the safe and proper interaction between concurrent web services. Most of the current tools focus on verification of existing formal models defined using specification languages such as BPEN (Business Process Execution Language), WS-CDL (Web Service Choreography Description Language), and recently, Conductor. We propose a framework for building formal models of web service architectures using an imperative programming language called WAFL - Web Architecture Formal Language. We also provide a way to define temporal logic properties based on assertions defined using WAFL. The implementation of the framework was realized using the Maude rewrite logic language as an extension to the language itself. The advantage of such a framework is that it provides a way for software developers to model web service architectures without knowledge of formal modelling languages and with little understanding of formal verification.