Prototyping or modeling an application design is a useful approach for proving and analyzing an application before it goes to development and deployment. This paper describes a project that models and analyzes Web services.

The modeling technique uses a divide-and-conquer approach to split a Web service into operational and control behaviors. Operational behavior describes business logic; control behavior sequences through various operational behavior components in response to internal and external stimuli. The two components are reunited in a hierarchy. The control and operational behaviors are each specified as statechart-like finite state machines (FSMs), with individual states in the control behavior mapping to FSMs in the operational behavior. The hierarchy between control and operation is bridged via conversation messages, the sequencing of which defines the overall behavior of the Web service.

Once modeled, a Web service can be analyzed in terms of its soundness and completeness--concepts that are introduced but not distinguished in terms of predicates over conversation message sequences. A graphical tool, which was developed as part of the project, constructs the models and analyzes--or at least traces--them through possible conversation message sequences.

The paper requires a modest familiarity with FSM formalism, but no particular knowledge of Web services. A background in automated analysis would be helpful in picking up on the project’s intentions, but may lead to overestimating the project’s scope. Although short, the bibliography lists relevant background papers.