SAS is a top-down specified conversation protocol in Guarded Automata (GA). SAS example is located at directory wsatDemo-1.0/Samples/GA_Protocol/SAS of the demo package. The SAS example is a case study given in [ISSTA'04], for the presentation of the techniques to handle bounded XML data and XPath based data manipulation in the formal verification process. In the following, we briefly introduce the control/data logic of the SAS example, and show how to use WSAT to analyze SAS.
Go to the directory wsatDemo-1.0/Samples/GA_Protocol/SAS, SAS protocol is presented in the file SAS.spec.
As shown in the following figure, there are three peers involved in the protocol: an investor, a stock broker, and a research department. The figure also describes the abstract control flows of the conversation protocol: First, the investor sends the stock broker a register message, which consists a list of stockID's that the investor has interests. After the registration is accepted, the stock broker will try to relay the requests to the research department, but only one stockID is sent per request. So there is an iteration of request from stock broker to research department --> report from research department to investor --> ack from investor to stock broker. Note that during the iteration, the investor has the right to cancel the whole service. When every stockID is processed, the broker bills the investor and terminates the research department.
Now we discuss the data manipulation semantics of SAS. Examine the SAS.spec, the XPath guards of transition t8 and t14 are important for the protocol to decide when to terminate the request/report/ack iteration. The two transitions are shown as below. Basically, t8 checks ``if the stockID in the last request is NOT the last stockID in the register information sent by investor", then t14 will try to locate the subsequent stockID in the register information and send it in the request message being sent. Transition t14 checks ``if the stockID in the most recent request message IS the last stockID in the register message'', then it will send out the bill message and conclude the conversation.
t8{ s8 -> s9 : request,
Guard{ $request//stockID != $reginfo//stockID [position() = last()] =>
$request[
//orderID:= $reginfo//orderID,
//stockID:= $reginfo//stockID [position() =
$reginfo//stockID[/. = $request//stockID]/position() + 1]
}
},
t14{ s8
-> s12 : bill,
Guard{
$request//stockID = $reginfo//stockID [position() = last()] =>
$bill[
//orderID:= $reginfo//orderID
]
}
},
We now first check the realizability of the SAS protocol. Type the following command:
java wsat -a -GA SAS.spec
In the above command, "-a" means to apply the analysis, and "-GA" means the input is specified using Guarded Automaton. The following is the output of SPIN. The realizability analysis for SAS reports that the skeleton of the protocol satisfies three realizability conditions, and the GA protocol itself satisfies a deterministic guards condition, which leads to the realizability of the SAS protocol. According to [ICWS'04], from the SAS protocol we can synthesize peer implementations for investor, stock broker and research department via projection.
Now we discuss the LTL model checking of the SAS example. The proposed (desired) system property of SAS example is located at property.pml, basically this property requires that " if nothing wrong happens, i.e., neither the investor cancels the deal nor the broker rejects the register request, then if there is some stockID appears in the initial register information, it should eventually appear in some request message from the stock broker to research department." In the following, we will check if the property is satisfied. Type the following commands:
cat output.pml property.pml > test.pml
spin -a test.pml
gcc -o pan pan.c
./pan -a
The above "cat" command concatenate the Promela code (output.pml) with the property. Note that the output.pml is the Promela translation generated by WSAT. Then "spin -a" generate the specialized model checker for SAS in C code (pan.c). We compile pan.c and run the model checker with the command ".pan -a", and the following is the spin output.
As shown in the above figure, SPIN identified an error after reaching 232 steps' depth, and 404543 states. Now we discuss how to generate and analyze the error trace generated by SPIN. Now that at this moment, you should find a file called test.pml.trace in the SAS directory. Now we examine the values of local and global variables at the final state. Type the following command:
spin -tlg test.pml
We get the following figure. Note that the values of the three stockID's in the reginfo message (their values are 0,1,0 respectively). These are also the values of the reginfo message at the init stage of the protocol, because no transitions in the protocol change their value during the whole execution process. Later, we will show that these initial values for reginfo message cause the error.
Now we want to examine what transitions are taken in the error trace, type the following command:
spin -t -l -g -p test.pml | grep "msg ="
We get the following results. In the Promela translation for each transition in the GA protocol, there is an assignment which assigns a global variable "msg" with the name of the current message being sent (e.g. m_reginfo). Study the following screen snapshot, you will notice that the request/report/ack iteration is only executed ONCE, and stockID with value 1 is skipped and never processed during the interaction! The reason is that stockID value 0 is also the LAST element of reginfo, and when transition t14 sees it, it simply sends out the bill to terminate the conversation and ignores the second element in the requestlist of the reginfo message. This leads to the violation of the proposed LTL property.
