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
You can also use the autoOff-lightcontroller framework from the tron package as basis and specify, model and implement your own non-trivial light controller like device
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 or Uppaal assisted) 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 RT-IOCO conforming to the specification, i.e. killable by some test case. The errors may of course both involve logical errors as well as timing. Use your imagination and create plausible mutants that could result from real coding errors.
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?).
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 preferably also the 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, implemented as automata and executed by TRON as illustrated by the cover test automaton as instructed below.
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)
- TRON. Please download and install according to the Tron webpage. Then read the instructions in the readme.txt file (also found in the tron package) to start tron.
If you use CS linux server hosts (simpsons) beware that each group uses distinct sets of tcp ports!
Instructions (execution of offline generated tests):
We recommend executing your preset input sequences using TRON by modeling the test input sequence as a timed automaton and by replacing the environment with this automaton. An example is provided in LightContr4.xml (Template: LightCov and Envy Closure. See system section).
The difference bwteeen LightContr.xml and LightContr4.xml is that LightContr.xml contains a model of the adaptor, and more options for configuring tolerances important for real-time execution, but is also more complex. For the simulated clock framework the simpler model and a tolerance of 1 as in the LightContr4.xml suffice. Beware of the tolerances allowed by the test specification if you cannot kill a time-based mutant.
Start tron as described below. You can also try different guide options for randomization (-P option, see tron --help):The command line options mean the following: Start tron using "SocketAdaptor" adaptor to communicate with IUT, 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 hints how uppaal-TRON should select inputs at random times within environment behavior : The options given after -- are handed to the adaptor component rather than tron itself. -v indicates the verbosity level, ie the amount of printed information on the console.
- marge [~/tron-1.4a/smart-lamp]:../tron -Q 6521 -P 10,200 -F 300 -I SocketAdapter -v 10 -w 20 LightContr4.xml -- localhost 9999
- marge [~/tron-1.4a/smart-lamp]:. ./tron -Q 6521 -P random -F 300 -I SocketAdapter -v 8 LightContr4.xml -- localhost 9999 silent
- marge [~/tron-1.4a/smart-lamp]:../tron -Q 6521 -P eager -F 300 -I SocketAdapter -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 as in the above instructions)
- 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.