Overview

• The WebVerdi-M system offers a rewriting-based Web verification service, which is able to recognize forbidden/incorrect patterns as well as incomplete/missing Web pages. WebVerdi-M relies on a powerful Web verification engine (called Verdi-M) that is written in Maude, which automatically derives the error symptoms. Thanks to the AC pattern matching supported by Maude and its metalevel facilities, WebVerdi-M enjoys much better performance and usability than a previous implementation of the verification framework. By using the XML Benchmarking tool xmlgen, we develop some scalable experiments which can be found here.



• WebVerdi-M has a service-oriented architecture that allows one to access the core verification engine Verdi-M as a reusable entity. WebVerdi-M can be divided into two layers: front-end and back-end. The back-end layer provides web services to support the front-end layer. This architecture allow clients on the network to invoke the Web service functionality through the available interfaces. The tool consists of the following components: Web service WebVerdiService, Web client WebVerdiClient, core engine Verdi-M, XML API, and database DB.
  
  The next figure illustrates the overall architecture of the system.

  

  WebVerdiService

  Our web service exports six operations that are network-accessible through standardized XML messaging. These operations are: store a Web site, remove a Web site, retrieve a Web site, add Web page to a Web site, check correctness, and check completeness. The Web service acts as a single access point to the core engine Verdi-M which implements our Web verification methodology in Maude. Following the standards, the architecture is also platform and language independent.

  XML API

  In order for successful communications to occur, both the WebVerdiService and WebVerdiClient (or any user) must agree to a common format for the messages being delivered so that they can be properly interpreted at each end. The WebVerdiService Web service is developed by defining an API that encompasses the executable library of the core engine. This is achieved by making use of Oracle JDeveloper, including the generation of WSDL for making the API available. The OC4J Server (the web server integrated in Oracle JDeveloper) handles all procedures common to Web service development. Synthesized error symptoms are also encoded as XML documents in order to be transferred from the WebVerdiService Web service to client applications as an XML response by means of the SOAP protocol.

  Verdi-M

  Verdi-M is the most important part of th3e tool. Here is where the verification methodology is implemented. This component is implemented in Maude language and is independent of the other system components.

  WebVerdiClient

  WebVerdiClient is a Web client that interacts with the Web service to use the capabilities of Verdi-M. Our main goal was to provide an intuitive and friendly interface for the user. WebVerdiClient is provided with a versatile, new graphical interface that offers three complementary views for both, the specification rules and the pages of the considered Web site: the first one is based on the typical idea of accessing contents by using folders trees and is particularly useful for beginners; the second one is based on XML, and the third one is based on term algebra syntax. The tool provides all translations among the three views.

  DB

  The WebVerdiService Web service needs to transmit abundant XML data over the Web to and from client applications. The common behavior of a user when using the tool is to modify the default rules provided for the Web specification and then verify a particular Web site. After modifying the Web specification, it would be necessary to send back to the service the considered specification as well as the whole Web site to verify. After the application invokes the WebVerdiServiceWeb service with these two elements, synthesized errors are progressively generated and transferred to the client application. The standard Web service architecture requires client applications to wait until all data are received and then errors are sent, which could cause significant time lags in the application. In order to avoid this overhead and to provide better performance to the user, we use a local MySql data base where the Web site and Web errors are temporarily stored at the server side.