Publications: Composition
Preference Reasoning

Contact:

The research activities of the group are supported in parts by US National Science Foundation grants CCF 0702758.

Members

Faculty: Samik Basu

Students: Zachary Oster (PhD): Requirements Analysis and Preferences

Abstract

We study the problem of substitution of components in a composite service, especially in the setting where the substitute is composed in an asynchronous fashion. By asynchronous composition, we mean that the participants in the composition are not required to synchronize on the input/output actions as long as the input to one participant always follows the corresponding output from another. We show that such asynchronous composition can be realized by synchronous composition of the participating components along with an appropriate buffer process. The buffer process is responsible only for relaying inputs from one component to another as and when needed; it is incapable of generating actions. Using this realization of synchronous composition with buffering, we obtain the condition which, when satisfied by a component (say Q'1), allows it to act as a correct substitute for Q1 in a composition of Q1 and Q2. Our work extends prior results on substitutability where the conditions relied on synchronous composition and/or on the structural equivalence between the substitute and the component being replaced.

Download full paper from IEEE Xplore or IEEE CS Digital Library


Tool Description

Download the tools and a sample input file (zip format, approximately 108K)

No installation is necessary; simply unzip the zip file into any directory.

You can also download our Java source code (zip format, approximately 128K) and build the tools yourself. When you unzip this file, it will create its own new directory. You can then import the code from this directory into a new project in Eclipse (or whatever IDE you prefer).

Please note that this is a "pre-beta" release of this tool. It has all of the capabilities that we presented in the paper, but the user interface is limited and it may have a few small bugs remaining. In future work, we plan to incorporate these tools into a more complete (and possibly GUI-equipped) framework for Web service substitutability analysis.

Requirements

The Java SE 6 runtime environment (JRE version 1.6.x) must be installed to run these tools. The XML input/output functionality for these tools is based on StAX (Streaming API for XML), which is not included in earlier Java versions; as a result, the tools will (probably) not work with earlier versions of the JRE. If you have the most recent version of the JRE, you should have no problems.

There are no other requirements.

Using the tool

Using either tool is a simple process.

XMLinput/output file format

We do not use a formal XML Schema (.xsd) document to validate our input, but we do make some assumptions about the layout of the file. Essentially, the format we use looks like this:
 <?xml version="1.0"?> <quotienting-data>
  <services>
    <service name="[name]">
      <states>
        <state name="[name]" isStart="{true|false}" isFinal="{true|false}" />
	.
	.
	.
      </states>
      <actions>
        <action name="[name]" type="[?|!|TAU|]" />
	.
	.
	.
      </actions>
      <transitions>
        <transition name="[name]" startState="state-name" endState="state-name" action="action-name" />
	.
	.
	.
      </transitions>
    </service>
    .
    .
    .
  </services>
  <restriction-set>
    <action name="[name]" type="[?|!|TAU|]" />
    .
    .
    .
  </restriction-set>
  <property>
    <!-- Any of the following elements can contain other elements. -->
    <fixpt-formula type="mu|nu" variable="fixpt-var-name">
    </fixpt-formula>

    <diamond action="full-action-name">
    </diamond>

    <box action="full-action-name">
    </box>

    <and-formula>
      <left>
      .
      .
      .
      </left>
      <right>
      .
      .
      .
      </right>
    </and-formula>

    <or-formula>
      <left>
      .
      .
      .
      </left>
      <right>
      .
      .
      .
      </right>
    </or-formula>

    <!-- The following two element types cannot contain other elements. -->
    <proposition name="[name]" />
    <fixpt-variable name="fixpt-var-name" />

  </property>
</quotienting-data>
Top of page

Full quotienting results from the paper

In both examples shown below, quotienting is performed against the same formula:

φ = 〈loaninfo?〉 μX.(〈ssn?〉 μY.(〈decision!〉tt ∨ 〈τ〉Y) ∨ 〈τ〉X)
To improve readability, we divide this formula into several subformulas:
φ = 〈loaninfo?〉φ1
φ1 = μX.(〈ssn?〉φ2 ∨ 〈τ〉X)
φ2 = μY.(〈decision!〉tt ∨ 〈τ〉Y)

Figure 5 Q_2

In the paper, Figure 5 shows the result of (φ /∅,R Q2), or quotienting the formula φ against the LTS Q2 (shown above). Although the results shown in Figure 5 are correct, we left a few lines out of those results to save space. We now show here the full quotienting process for this example.

Note that quotienting of a mu-calculus formula against an LTS is equivalent to quotienting of a formula against the start state of the LTS. This means that (φ /∅,R Q2) ≡ (φ /∅,R t1). Also note that quotienting a fixed-point variable against a state is equivalent to quotienting that variable's definition against a state. This means that (X /∅,R t1) ≡ (φ1 /∅,R t1) and that (Y /∅,R t1) ≡ (φ2 /∅,R t1).

The steps of the quotienting process proceed as follows. Rule numbers correspond to the quotienting rules given in Figure 4 of the paper.

(φ /∅,R t1) = 〈loaninfo?〉(φ1 /∅,R t1) Rule 5
1 /∅,R t1) = μX1t1.(〈ssn?〉(φ2 /{X1t1},R t1) ∨ 〈τ〉X1t1 ∨ 〈rate!〉(X /{X1t1},R t2))
Rules 7 and 5
(X /{X1t1},R t2) = μX1t2.(〈ssn?〉(φ2 /{X1t1, X1t2},R t2) ∨ 〈τ〉X1t2 ∨ 〈credscr!〉(X /{X1t1, X1t2},R t3))
Rules 8, 7, and 5
(X /{X1t1, X1t2},R t3) = μX1t3.(〈ssn?〉(φ2 /{X1t1, X1t2, X1t3},R t3) ∨ 〈τ〉X1t3 Rules 8, 7, and 5
2 /{X1t1},R t1) = μY1t1.(〈decision!〉tt ∨ 〈τ〉Y1t1 ∨ 〈rate!〉(Y /{X1t1, Y1t1},R t2))
Rules 7 and 5
(Y /{X1t1, Y1t1},R t2) = μY1t2.(〈decision!〉tt ∨ 〈τ〉Y1t2 ∨ 〈credscr!〉(Y /{X1t1, Y1t1, Y1t2},R t3))
Rules 8, 7, and 5
(Y /{X1t1, Y1t1, Y1t2},R t3) = μY1t3.tt Rules 8, 7, 5, and 1

Figure 7

Q_B12

Figure 7 in the paper presents part of the result of (φ /∅,R QB12), or quotienting the formula φ against the LTS QB12. This LTS, shown above, represents the buffer service created from the restriction set {rate?, rate!, credscr?, credscr!}. A buffer service created for any restriction set that contains two matching pairs of actions will have the same structure.

There was not enough space in the paper to show the complete quotienting process for this example, so we show the full result here:

1 /∅,R QB12) = 〈loaninfo?〉μX1b1.
(〈ssn?〉μY1b1.
(〈decision!〉tt
∨ 〈rate!〉μY1b2.
(〈decision!〉tt
∨ 〈rate?〉μY1b3.
(〈decision!〉tt
∨ 〈credscr!〉μY1b4. (〈decision!〉tt ∨ 〈credscr?〉μY1b5. (〈decision!〉tt ∨ 〈τ〉Y1b5 ) ∨ 〈τ〉Y1b4 )
∨ 〈τ〉Y1b3 )
∨ 〈credscr!〉μY1b6.
(〈decision!〉tt
∨ 〈rate?〉Y1b4
∨ 〈credscr?〉μY1b7. (〈decision!〉tt ∨ 〈rate?〉Y1b5 ∨ 〈τ〉Y1b7 )
∨ 〈τ〉Y1b6 )
∨ 〈τ〉Y1b2 )
∨ 〈credscr!〉μY1b8.
(〈decision!〉tt
∨ 〈rate!〉Y1b6
∨ 〈credscr?〉μY1b9. (〈decision!〉tt ∨ 〈rate!〉Y1b7 ∨ 〈τ〉Y1b9 )
∨ 〈τ〉Y1b8 )
∨ 〈τ〉Y1b1 )
∨ 〈rate!〉μX1b2.
(〈ssn?〉μY2b2. (〈decision!〉tt ∨ 〈rate?〉Y1b3 ∨ 〈credscr!〉Y1b6 ∨ 〈τ〉Y2b2 )
∨ 〈rate?〉μX1b3.
(〈ssn?〉μY2b3. (〈decision!〉tt ∨ 〈credscr!〉Y1b4 ∨ 〈τ〉Y2b3 )
∨ 〈credscr!〉μX1b4.
(〈ssn?〉μY2b4. (〈decision!〉tt ∨ 〈credscr?〉Y1b5 ∨ 〈τ〉Y2b4 )
∨ 〈credscr?〉μX1b5. (〈ssn?〉μY2b5. (〈decision!〉tt ∨ 〈τ〉Y2b5 ) ∨ 〈τ〉X1b5 )
∨ 〈τ〉X1b4 )
∨ 〈τ〉X1b3 )
∨ 〈credscr!〉μX1b6.
(〈ssn?〉μY2b6. (〈decision!〉tt ∨ 〈rate?〉Y2b4 ∨ 〈credscr?〉Y1b7 ∨ 〈τ〉Y2b6 )
∨ 〈rate?〉Y1b4
∨ 〈credscr?〉μX1b7. (〈ssn?〉μY2b7. (〈decision!〉tt ∨ 〈rate?〉Y2b5 ∨ 〈τ〉Y2b7 ) ∨ 〈rate?〉X1b5 ∨ 〈τ〉X1b7 )
∨ 〈τ〉X1b6 )
∨ 〈τ〉X1b2 )
∨ 〈credscr!〉μX1b8.
(〈ssn?〉μY2b8. (〈decision!〉tt ∨ 〈rate!〉Y2b6 ∨ 〈credscr?〉Y1b9 ∨ 〈τ〉Y2b8 )
∨ 〈rate!〉X1b6
∨ 〈credscr?〉μX1b9. (〈ssn?〉μY2b9. (〈decision!〉tt ∨ 〈rate!〉Y2b7 ∨ 〈τ〉Y2b9 ) ∨ 〈rate!〉X1b7 ∨ 〈τ〉X1b9 )
∨ 〈τ〉X1b8 )
∨ 〈τ〉X1b1 )

Top of page