UIMDRIVER: UML Interaction Model Driven Runtime Verification
Introduction Download Case Study 1

Case Study 1

Case studies One

Download the case

Download the demo

The first example is an automated teller machine simulation system, which is a complete example of object-oriented analysis, design, and programming applied to a moderate size problem. The detailed documentations about analysis, design, and implementation are given in [1]. As depicted in Figure 1, a sequence diagram derived from transaction use case is selected to construct specifications, which describes the event flow that all the individual types of transaction (withdrawal, deposit, transfer, inquiry) must conform to. It includes two successive scenarios: the first is the business logic of one transaction in which the messages getSpecificsFromCustomer, selectTransaction, and getMenuChoice occur in the proper order; the second is the transaction tracing process which consists of receipt printing and information logging.

Based on the sequence diagram, an an exceptional consistency specification is constructed. It is constructed by exchanging the positions of message logSend and logResponse in the sequence diagram, which violates the requirement that messages sent to the bank should be logged first and then messages got from the bank are logged, and forms a forbidden scenario in the program.

A backward mandatory consistency specification is built as well. It is by splitting the sequence diagram, which indicates that a transaction can not enter the tracing process until its corresponding business process has been completed.

Figure 1: The sequence diagrams and specifications in the ATM system

The experiment process is as follows. In one experiment, the tool drives the system execution 20 times with random test cases, and check the program execution traces for the specifications. After the experiment conducts 30 times, the tool reports no inconsistent case. Then, we embed manually a bug in the program by changing the order of the events corresponding to message logSend and logResponse. The experiment conducts 30 times again, and each time the tool drives the program execution 20 times with random test cases. The result is that the tool finds out the inconsistent case in each experiment. Figure 16 depicts how many times the program has been executed in each experiment when the first inconsistent case is detected.

 

Figure 2: The experimental results of the ATM system

 

 

[1]  Russell C. Bjork. The Simulation of an Automated Teller Machine. Links


©2010 SEG CS NJU IntroductionDownloadCase Study 1