ATM Example

The first example is the automatic teller machine (ATM) system is [1] whose specification is depicted in Figure 1. We will introduce the SBS first then we'll show the experiment data.

Scenario-based specification for the ATM example

The ATM system consists of the three components: potential customers (process User), the ATM controller (process ATM), and a host computer in a bank (process Bank). Initially, the ATM controller waits to receive the customer’s bank card and requests a pin number in [0, 2] seconds after receiving a card (0≤b₁-a₂≤2, SDs StartTrans and GetPin). Then, it either receives a request to cancel the transaction within [0, 4] seconds (0≤c₂-b₁≤4, SD EndTrans), or receives the customer's pin number within [5, 60] seconds (5≤d₂-b₁≤60, SD ProcessPin). If the ATM receives a request to cancel the transaction, it returns the customer’s card and takes [2, 3] seconds to return to its initial state (2≤ω_c-c₃≤3, SD EndTrans).  The ATM expects a reply from the bank within 10 seconds, which is represented by the following timing constraints:

            0≤f₂-d₃≤10,        0≤g₂-d₃≤10,       0≤j₂-h₇≤10
            0≤k₂-h₇≤10,       0≤i₆ - i₃≤10,       0≤ j₈- j₅≤10.

If no reply from the bank is received in a delay of 10 seconds, the card is returned, an appropriate message is then displayed, and the ATM takes [2, 3] seconds to return to its initial state (e₁-d₃=10, 2≤ω_e-e₅≤3, SD TryAgain). The specification also describes the following constraints:

• a customer expects a withdraw request to be processed within [0, W] seconds relative to the time of entering an amount (0≤j₄-h₅≤W, 0≤k₄-h₅≤W);

• the ATM takes [B₁, B₂] seconds for book-keeping after dispensing cash (B₁≤ω_j-j₉≤B_2, SD DispenseCash);

• the ATM takes [3, 5] seconds to print a receipt after receiving the balance information from the bank (3≤j_b-j₈≤5, 3≤i₉-i₆≤5, SD DispenseCash, SD GetBalance); and

• in the case of refusing pin number, at the first time the ATM takes [0, 2] seconds to request a pin number again after sending the information for the invalid pin number (0≤b₁-g₂≤2), and at the second time it takes [3, 5] seconds to confiscate the card and inform the customer (3≤l₁-g₃≤5, SD ConfiscateCard).

Each ATM-customer communication takes at least T₁ seconds, and each ATM-bank communication takes at least T₂ seconds, which we do not explicitly represent in the chart.

Figure 1 Scenario-based specification for the ATM example

For timing analysis of the ATM specification depicted in Figure 1, TASS is used to solve the following problems:

• Reachability analysis: we check if the node SD DispenseCash is reachable in the specification.

• Constraint conformance analysis: since a customer may lose his patience after he gets the money, we require that the time that the ATM takes for the printing and book-keeping after giving the money is not greater than the half of the time that the customer waits for withdrawing the money (2( ω_j-j₈)≤j_c-h₅), which forms a constraint conformance specification Sc(ρ, ζ) where ρ = Withdraw^DispenseCash, and ζ = 2( ω_j-j₈)≤j_c-h₅.

• Bound delay analysis: since for security consideration it is necessary to record the process for withdrawing money by the camera embedded in the ATM, we require every process for withdrawing money take the time which is long enough for recording, which forms a minimal bounded delay specification S_B^m(j₄, a₁, 20).

Experiment Data

We created four cases with various values for W, B₁, B₂, T₁, and T₂. Then we analyzed the ATM SBS with both synchronous and asynchronous composition semantics. All the experiments were conducted on a Pentium 4 /2.2GHz/2.0GB PC.

First we run all three timing analyzers with synchronous composition semantics. In the loop-unlimited timing analysis mode we first checked if the SBS is loop-unlimited. If so, we run the loop-unlimited timing analyzer to check the SBS. The results in table 1 shows that TASS runs comfortably for checking SBSs with 16 SDs in a few seconds.

Table 1: Sample results of loop-unlimited timing analysis of the ATM specification

with synchronous composition semantics

In path-oriented analysis mode, we checked the path “StartTrans → GetPin → ProcessPin → GetOption → (Withdraw → RefuseWith)^k → Withdraw →DispenseCash → EndTrans”, which indicates a scenario that after k times of refusing withdraw the ATM can still conduct a correct dispense cash operation. It was shown that while the length of this path can be as long as 800 (400*2) steps with the amount of constraints reaching to 13696 and the amount of variables reaching to 6445 TASS could finish the computation within one and a half hours. The results in Table 2 was conducted on case 3.

Table 2. Sample results of path-oriented timing analysis of the ATM specification

with synchronous composition semantics

In the bounded timing analysis we checked the paths of SBS one by one until the length of the path reaches to a given threshold. We set k to 20 so that the number of paths checked accumulates to 36704. Moreover we observed that during the computation TASS consumed no more than 30MB of memory. This advantage comes from our DFS manner in traversing the specifications. Since TASS can do the analysis without manual interference, given enough time it is possible to check a large amount of paths. The results data are shown in Table 3 which was conducted on case 4.

Table 3. Sample results of bounded timing analysis of the ATM specification

with synchronous composition semantics

For asynchronous composition semantics we also conducted two experiments. In the path-orientd timing analysis mode we checked the path “StartTrans → GetPin → ProcessPin → GetOption → (Withdraw → RefuseWith)^k → Withdraw →DispenseCash → EndTrans”. The results shown in Table 4 were conducted on case 3.

Table 4. Sample results of path-oriented timing analysis of the ATM specification

with asynchronous composition semantics

At last we applied the bounded timing analysis to the ATM specification case 4. The results is shown below.

Table 5. Sample results of bounded timing analysis of the ATM specification

with asynchronous composition semantics

[1] Hanene Ben-Abdallah and Stefan Leue. Timing Constraints in Message Sequence Chart Specifications. In Proceedings of FORTE/PSTV’97, Chapman & Hall, 1997.