WS-RV—Runtime Verification for Web Services

WS-RV is a framework to integrate Runtime Monitoring seamlessly into Service Oriented Architectures and othere environments using XML Web Services as middleware. WS-RV is based on the Java API for XML Web Services (JAX-WS). The basic concepts of the framework are Interceptors, Monitoring Services and Monitors. Interceptors can be attached to the Java Webservices Stack and send messages to Monitoring Services. Monitoring Services can be deployed to arbitrary Web Service Containers and mangage serveral monitors. Monitors check the observed sequence of message with respect to some temporal correctness properties. These properties are specified in a high level language based on XML and are automatically synthesised during initialisation of the corresponding monitoring service.

Appetizer

Consider the property, that certain messages have to be processed in their sending order:

G(i = sendNum ⇒ X sendNum > i)

You can integrate monitoring for that property in your enviroment with the following four steps:

1. Define Monitors

Monitors are described using XML. A monitor for the property above can be described as follows:

<monitors>
    <monitor>
        <name>SendOrder</name>
        <solverName>Z3</solverName>
        <filter>
            //*:direction/text() = "receive"
            and //*:sendInterceptor/text() = "mic"
            and //*:receiveInterceptor/text() = "dis"
        </filter>
        <formula class="R">
            <FALSE/>
            <OR>
                <NOT>
                    <P>
                        <sym>
                            <xquery><![CDATA[
                                <eq><intVar>x</intVar><int>
                                    {xs:integer(//*:sendSequenceNumber/text())}
                                </int></eq>
                            ]]></xquery>
                        </sym>
                    </P>
                </NOT>
                <WX>
                    <P>
                        <sym>
                            <xquery><![CDATA[
                                <lt><intVar>x</intVar><int>
                                    {xs:integer(//*:sendSequenceNumber/text())}
                                </int></lt>
                            ]]></xquery>
                        </sym>
                    </P>
                </WX>
            </OR>
        </formula>
    </monitor>
</monitors>

2. Publish Handler Service

The Monitoring Service can send its output to a handler service. The framework provides a simple implementation logging the output, but a custom implementation may be used to react to failures appropriately.

Endpoint.publish("http://localhost/mylogger",
    new RVLoggerWS(Logger.getGlobal()));

3. Publish Monitoring Service

Finally, the Monitoring Service has to be instantiated using the specification above.

Endpoint.publish("http://localhost/mymonitor",
    create("http://localhost/mylogger", new URL("file:///somewhere/specification"));

4. Attach Interceptors

When publishing services you have to attach an Interceptor to the respective Endpoint. Many frameworks allow to do this via configuration. The Interceptor can also be attached using JAX-WS:

Endpoint endpoint = Endpoint.publish("http://localhost/myservice", new MyService());
Handler rvi = new RVInterceptor("dis",
    new InterceptionDescriptor("http://localhost/mymonitor", "true()", "true()"))
endpoint.getBinding().setHandlerChain(Collections.singletonList(rvi));

Now, your Web Services work as they did before but their message exchange will be monitored.

Download

WS-RV.zip

Installation

• Download and unzip the package above
• The package contains some examples as well as the source code of the web service frontend
• If you require Z3 support or want to run the benchmarks, Z3 has to be installed seperately
• All other dependencies are contained in the archive
• Java 7 is required

Contact

If you have further questions, problems using WS-RV or want to extend WS-RV in some way and need access to its source code, feel free to contact Daniel Thoma.

OR.NET

The project WS-RV was undertaken partly in the scope of our engagement in the project OR.NET.