Formal methods for data-centric web services: From model to implementation

Web services allow organizations to capture their human and software-based capabilities as modular software components that are called remotely over a network. In such service-oriented settings, it is important to establish an agreement that sets the obligations of the service provider and the expectations of the service consumer. Since traditional approaches such as Service Level Agreements (SLAs) are loosely defined with respect to data integrity aspects, in previous work, we proposed a formal model for specifying data-centric Web services. The goal is to formally and unambiguously specify the service behavior in terms of its underlying data model and data interactions. In this paper, we present our model and our effort in specifying and verifying data-centric Web services using three state-of-the-art specification languages: JML, Dafny and RESOLVE. Our goal is to study the feasibility of our proposed model and also to pinpoint the challenges and limitations of current specification and verification tools.