uk.ac.sheffield.vtts

Class VerifyProtocol

java.lang.Object

uk.ac.sheffield.vtts.VerifyProtocol

public class VerifyProtocol
extends java.lang.Object

Program that reads an XML service specification and checks the protocol of the service for input and memory completeness and deterministic behaviour. Use this program to analyse the protocol directly, after the accompanying state machine has already been validated. Warnings are given for missing operation scenarios (that should exist, according to the state machine), for incompletely-initialised memory and for operations that are found to be either blocking, or non-deterministic, under certain input and memory conditions. An analysis is given of the input and memory space of each operation, showing which guarded scenario accepts which input. Warnings identify inputs that trigger no response, or multiple responses. Requires ASTReader, ASTWriter, ASTError, NodeError from the JAST package.

Version:

Broker@Cloud 1.0

Author:

Anthony J H Simons

Constructor Summary

Constructors

Constructor and Description
VerifyProtocol()

Method Summary

Methods

Modifier and Type	Method and Description
static void	main(java.lang.String[] args) Reads an XML service specification from the input file, and, if no faults are found, checks the protocol of the specification for input completeness.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

VerifyProtocol

public VerifyProtocol()

Method Detail

main

public static void main(java.lang.String[] args)
                 throws java.io.IOException,
                        java.lang.IllegalArgumentException,
                        org.jast.ast.ASTError,
                        org.jast.ast.NodeError,
                        SemanticError

Reads an XML service specification from the input file, and, if no faults are found, checks the protocol of the specification for input completeness. For every operation, creates a set of input partitions, which includes every guard and its complement. Then, determines whether each partition triggers exactly one response. If no response is triggered, or more than one response is triggered, this indicates a possible fault in the specification. Uses a symbolic subsumption checking algorithm, which is conservative.

Parameters:

args - the XML service specification file, containing a root Service node.

Throws:

java.io.IOException - if a file system related I/O error occurs.

java.lang.IllegalArgumentException - if an invalid argument is supplied.

org.jast.ast.ASTError - if an XML syntax error is found in the input.

org.jast.ast.NodeError - if marshalling or unmarshalling the model fails.

SemanticError - if a semantic error is detected in the model.