The SSCC (Service Scenario-based Consistency Checker) is implemented for verification of Web Services communications against scenario-based specifications.

  Web Services are message-driven, and each service can be viewed as a component, so we focus on the temporal orders of message exchanges among processes, and check the consistency of the message exchange sequence against the scenario-based specifications. Scenario-based specifications offer an intuitive and visual way of describing system requirements, and play an increasingly important role in the specification and design of systems. Since message exchange sequence is the property we concern, UML Sequence Diagrams are used as the scenario-based specifications, which form an important aspect of the behavior of Web Services.
  As a de facto standard by OASIS in Web Services standard suite, the Web Services Business Process Execution Language (WS-BPEL) can be used for behavior description and composition of Web Services. Since we want to check the consistency of message exchange sequence of Web Services against scenario-based specification, we use Petri nets to transform the message flow of Web Services.

  SSCC tool takes WS-BPEL, WSDL code and UML Sequence Diagram model in Rational Rose as its input. The WS-BPEL process is transformed into a Petri net (we name it WS-BPEL Petri net, BPN for short). To reduce the state space, simplifications on both WS-BPEL code and BPN are performed. The simplified BPN is then verified against the UML Sequence Diagram.