DT8021 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:

• Model Checking: We model a system of two traffic lights placed on the corners of a junction, where two 1-way roads meet.

Traffic lights can be either green or red. On each of these two roads at most 2 cars may arrive at most at any moment of time and they will pass only if they see the traffic light to be green. The traffic light will only turn from red to green if there is at least one car waiting and the other traffic light is already red.

• 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.

All deliverables are sent by email as a group to the lecturer.

Model Checking

Specify the network of timed automata representing the traffic lights and the cars; design and simulate 5 scenarios, specify and verify at least 3 correctness properties in UPPAAL’s temporal logic and verify them correct. While model-checking, if you notice mistakes in your initial model, please mention them and the process of correcting your model. You need to hand in a .zip file containing a pdf describing the timed automata, the scenarios (with screen shots of their sequence diagrams), the queries and the result of the queries (including any changes made to the model to make it satisfies the queries).

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.