|
|
|
| Untersuchte Arbeit: Seite: 60, Zeilen: 1-9 |
Quelle: Schäfer et al 2001 Seite(n): 4-5, Zeilen: 4:40ff. - 5:1-5 |
|---|---|
| Figure 2.14: State Machine of the atm in ATM
As shown in Fig. 2.13, the bank computer validates the bank card concurrently to the PIN code. If the card is not valid, the concurrent validation is exited immediately and the ATM is requested to abort the transaction. The completion transition leaving VerifyingPIN simulates any possible PIN entry by branching non-deterministically into the states PINCorrect and PINIncorrect. The two join transitions evaluate the results of the concurrent validations. If an incorrect PIN has been entered and the card is valid, the counter of invalid PIN entries is incremented; however, if the counter numIncorrect exceeded a maximum value, the card is invalidated and the transaction aborted. In contrast, if a correct PIN has been entered, the counter is reset to zero [SKM01]. [SKM01] Tim Schaefer, Alexander Knapp, and Stephan. Merz. Model checking uml state machines and collaborations. In Scott D. Stoller and Willem Visser, editors, Proc. Wsh. Software Model Checking, volume 55(3) of Electr. Notes Theo. Comp. Sci., 2001. 13 pages. |
[page 4]
As shown in fig. 1(e), the bank computer validates the bank card concurrently to the PIN code. If the card is not valid, the concurrent validation is exited immediately and the ATM is requested to abort the transaction. The completion transition leaving VerifyingPIN simulates any possible PIN entry by branching non-deterministically into the states PINCorrect and PIN- [page 5] Incorrect. The two join transitions evaluate the results of the concurrent validations. If an incorrect PIN has been entered and the card is valid, the counter of invalid PIN entries is incremented; however, if the counter has exceeded a maximum value, the card is invalidated and the transaction aborted. In contrast, if a correct PIN has been entered, the counter is reset to zero. [page 7] (d) State machine diagram for class ATM Fig. 1. UML model of an ATM |
Identical with no part of it being marked as a citation. The source is named in passing at the end of the paragraph. The figures also show identical state machine diagrams (though drawn slightly different). |
|