DIT085 Ed 2016 Practical Phase 3

Objectives

This phase of the project is designed to apply UI testing as well as formal (mathematical) modelling and verification techniques to a small case study:

• apply mathematical modelling to capture the core behavior of a concurrency scenario in accessing a shared communication channel,

• apply simulation to gain insight on some of its basic behavior,

• specify some of its correctness properties in a temporal logic,

• apply model checking to verify the properties of the modelled behavior, and

• apply Visual GUI testing to the Arduino-Odroid example.

General Description

We separate two activities in this phase; the second activity is optional, but it is necessary to get a VG:

• Model Checking: In the first activity, we focus on a model of two concurrent threads accessing a shared USB channel. Each thread would like to communicate two integer values (each ranging from 0 to 2) using the shared USB channel. The USB channel may be disconnected at any point and the information may not be communicated, in which case the thread will have to attempt the transmission of the same value again. Each of the threads and the communication channel should be modelled as a separate automata and use of global shared variables is not allowed.

• Visual GUI Testing: In the second activity, you specify a few scenarios for testing the GUI of the your application from phase 2. Note that you may have to extend the UI from phase to make some of the testing scenarios possible (e.g., to disconnect the USB connection while testing). Then, perform Visual GUI testing using Sikuli (or any comparable tool) in order to test the main functionality of the system in terms of a few scenarios.

Deliverables

There are three main deliverables for this phase:

• a single pdf file documenting the outcome of each and every of the following activities,
• a .zip file containing the source code of the models (e.g., automata and queries) and the software implemented in different parts, and
• a self evaluation of your own effort and the effort by each and every member.

The first two deliverables are sent as a group using GUL. The last deliverable is sent by email by each member individually to both supervisors.

Model Checking

Specify the network of timed automata representing the concurrent threads and the USB channel. Specify 3 possible scenarios of interaction in the system (in plain English or using a sequence diagram) and simulate them in UPPAAL. Subsequently, formulate 3 correctness criteria for your design and model-check them in UPPAAL. While model-checking, if you notice mistakes in your initial model, please mention them and the process of correcting your model.

Visual GUI Testing

Design at least 5 scenarios of interaction (e.g., communication of ordinary values for different period lengths, attempt to enter out of range values in the GUI, and disconnecting USB channel during communication) and code them as scripts in Sikuli. Run the tests and make sure that all of them run successfully. Perform debugging if necessary.