top of page

The Formal Specification and Verification of Data-Centric Web Services

Web services are reusable software components that enable loosely-coupled business-to-business and customer-to-business interactions over the Web. Service consumers depend heavily on the service interface specification to discover, invoke, and synthesize services. Data-centric Web services are services whose behavior is determined by their interactions with a repository of stored data. A major challenge in this domain is interpreting the data that must be marshaled between consumer and producer systems. Current standard languages for describing Web services only specify a service operation in terms of its syntactical inputs and outputs; these languages do not provide a means for specifying the underlying data model, nor do they specify how a service invocation affects the data. The lack of data specification potentially leads to erroneous use of the service by a consumer. 

 

My work proposes a formal data contract for data- centric Web services. The contract is a set of formal assertions describing the service behavior with respect to its interaction with the data. The contract also exposes data-related business rules. The proposed approach is based on formal methods and design-by-contract principles; it hence provides a machine-readable specification of the service. This facilitates automatic analysis, testing, and reasoning about the service behavior. I empirically demonstrate through my research how the proposed formal contract can effectively decreases ambiguity about a service behavior and provides correctness and data integrity guarantees within a composition of services. I also use the formal contract to enhance the generation of unit tests for service-based applications. In this case, the contract serves as a set of rules that are fed into a parametric testing tool to automatically generate test cases with high code coverage. Figure 1 shows the general proposed framework that extends the Service-Oriented Architecture (SOA) to support modeling and contracting of data-centric Web services.

 

Publications

  • Iman Saleh, M.Brian Blake, Gregory Kulczycki and Yi Wei: “Formal Methods for the Specification and Testing of Data-Centric Web Services: A Case Study”, the International Journal of Services Computing, vol. 1, no. 1, pp.39-51, Oct-Dec 2013

  • Iman Saleh, Gregory Kulczycki, and M.Brian Blake, "Towards the Implementation of Bug-Free Database Applications: A Formal Approach", First International SIGMOD Workshop on Reliable Data Services and Systems, (SIGMOD RDSS'14), June 2014

  • ​Iman Saleh, Gregory Kulczycki, M.Brian Blake and Yi Wei, "Static Detection of Implementation Errors Using Formal Code Specification", 11th International Conference on Software Engineering and Formal Methods, SEFM'13, September 2013

  • ​Iman Saleh, Gregory Kulczycki, M.Brian Blake and Yi Wei, "Formal Methods for Data-Centric Web Services: From Model to Implementation", IEEE International Conference on Web Services, ICWS'13,  June 2013

  • Iman Saleh, Gregory Kulczycki and M.Brian Blake, "Formal Specification and Verification of Transactional Service Composition", 2011 IEEE World Congress on Services, SERVICES'11, July 2011

  • Iman Saleh, Gregory Kulczycki and M.Brian Blake, "Formal Specification and Verification of Data-Centric Service Composition", IEEE International Conference on Web Services, ICWS'10,  July 2010. Acceptance Rate 15.6%

  • Iman Saleh, "Formal Specification and Verification of Data-Centric Web Services", IEEE Services' PhD Symposium, July 2010

  • Iman Saleh, Gregory Kulczycki and M.Brian Blake, "Specification and Verification of Web Services Transactions", PhD Workshop on Innovative Database Research, SIGMOD'10, June 2010

  • Iman Saleh, Gregory Kulczycki and M.Brian Blake, "A Reusable Model for Data-Centric Web Services", 11th International Conference on Software Reuse, September 2009

bottom of page