The goal here is to evaluate/apply Uppaal-TRON on you own model and implementation. The deliverables consists of the model, implementation, adaptor source code, and a couple of text pages describing your experiences. How usable did you find the tool, how difficult was it to use, did you find any (perhaps seeded) errors etc. The exercise takes place in groups of approx 3, but may collaborate with other groups on the implementation work. However, separate reports are needed. The deliverables must be signed by each student who, by his signature, declares active and equal participation in preparation of the deliverables.
Make a simple java application (supposedly correctly) implementing your model. It will need to be equipped with a small socket interface. You may steal the one from the light controller and use that as starting point (will need modifications). If your model/implementation is time sensitive, it is strongly recommended that it implements the simulated time-framework as illustrated by the light-controller source.
With your modeling exercise as starting point modify the model to be testable for tron: clean separation of IUT-model an Environment-model into distinct (sets of automata) communicating via inputs and output event. Use tron to test your application
Objective
The objective is to evaluate the usability and effectiveness of two approaches to automated real-time testing: Manually assisted test purpose based test generation and full automatic randomized online testing. Each group is given a UppAal specification of the light controller, and an (assumed!) correct implementation in java, including two example mutants. The experiment proceeds in two phases: Preparation phase and evaluation phase.
In the preparation phase, each group will independently (manually) generate a set of test cases and a set of mutated implementations based on the given specification and implementation. Each group runs their test suite on their own mutants, and possibly extend it as desired. The mutants must be non-conforming to the specification, ie. killable by some test case.
In the evaluation phase, each group swaps mutants (java byte-code) and runs
their own test suite against the groups own and other groups mutants, collecting statistics with the results (which own/other mutants were killed).
applies UppAal-TRON (randomized online testing) to the collected mutants (e.g 10 runs per mutant)., again collecting statistics about the percentage of runs killing the mutants, and preferable duration of the test runs.
Expectations.
Each group is to hand in the following deliverables to be evaluated.
10 to 20 error-seeded mutants of the Light Controller application, with a short description explaining the seeded errors. Mutants made to the Light Controller must be implemented.
The test suite, including the material needed to generate it, e.g a list of timed traces, uppaal (annotated) models, reachability properties, simulation traces, java sources. Each test must be accompanied by a short description in the style of an informal test purpose (one line of text) for each test case.
The statistics of the evaluation phase for manually generated tests (if you have big problems with timing tolerances, try to at least to implement and execute a few ones). Alternatively you can implement them in TRON as illustrated by the cover test automaton in the package.
The statistics collected by running Uppaal-TRON.
A (max) 1 page summary with the lessons learned.
The deliverables must be signed by each student who, by his signature, declares active and equal participation in preparation of the deliverables
Software
- Java sources for Light Controller is distributed with tron, requires > java 1.5: /pack/j2sdk-1.5.0.01/bin/java)
- Java sources for TestLightController for programming hand crafted test cases in Java (simulated time not possible at this time!). However test-cases can be written as uppaal automata as indicated below.
- Uppaal deterministic Specification and queries (used for offline generated tests) (available in smart-lamp/Offline)
- Compilation and execution of UppAal-TRON: Copy the following your own home directory (Linux only!):
- Linux (Marge/Homer): Precompiled binaries for Linux are installed in /user/bnielsen/tron-1.4a.)
- LD_LIBRARY_PATH must include current dir. eg. (tcsh) "setenv LD_LIBRARY_PATH $LD_LIBRARY_PATH:."
- marge [~/tron-1.4a/smart-lamp]: make clean
- marge [~/tron-1.4a/smart-lamp]: make test-light-s
//this should compile the adaptor for your host, and start the lightdemo.Instructions (execution of offline generated tests):
Two options. Implement (real-time) test cases in java, or implement them in tron
- Derive test seqences for the Light Controller using uppaal, and implement them in Java (Mimic the examples in TestLightController.java" (available in smart-lamp/Offline/LightController) The light controller implementation and light controller test program is started by.
>java -classpath . LightController.LightController 0
This runs mutant 0.
> java TestLightController localhost 9999 1 (NB bug in protocol - to be fixed ASAP)
this executes test #1 on the LightController running on port 9999 the same machine. To avoid conflicts each group should use different port-numbers. This is hardcoded into the lightcontroller application - You can easily change this - chose an arbitrary legal tcp/ip port and recompile.
Compile with the following commands:
> javac LightController/*.java
> javac TestLightControler.javaIt is possible to execute preset input sequences using TRON by modeling the test input sequence as a timed automaton and by replacing the environment with this automaton, and executing tron in eager mode. An example is provided in LightContr4.xml (Template: LightCov and Envy Closure. See system section). Start tron as described below, or try eager option:
marge [~/tron-1.4a/smart-lamp]:../tron -Q 6521 -NP eager -F 300 -I lightcontroller -v 8 LightContr4.xml -- localhost 9999 silent
Instructions (execution of online generated tests):
- start the light controller (may be on a different host) a different port requires recompilation of the java-implementation: (port 6521 is used by the clock sync protocol), port 9999 is used to convey tests events)
java LightController/LightController -C localhost 6521 -M 0
- Start tron: using "lightcontroller" adaptor, using test specification "lightContr4.xml", testing a java lightcontroller-implementation running on host ip number (can also be either "localhost", a dns-name, or an ipnumber, -P options indicates that uppaal-TRON should select inputs at random times (within environment behavior
marge [~/tron-1.4a/smart-lamp]:. ./tron -Q log -NP random -F 300 -I lightcontroller -v 8 LightContr4.xml -- localhost 9999 silent
Instructions (Real-time problems):
Here are some tips that may reduce real-time scheduling problems (alternatively use simulated time)
- use lightly loaded machines
- use local isolated, single user computers, and and perferable 2 cpu machine (or two machines interconnected via cross cable)
- use lightly loaded multi-cpu machine
- use Linux Kernel 2.6 (marge, not homer)
- Disable "Nagle's" algorithm by setting the socket option: setTcpNoDelay(true); This should already be done in all the applications and adaptors you will work with, including the "TestLightController" application.
- Do not X-tunnel the lightcontroller gui. If you cannot run the lightcontroller locally, try to remove GUI from Java Lightcontroller implementation by uncomment the code that create the graphics objects: run the light controller with -N option.