Download test

TRON
TRON
Real Time Testing
using UPPAAL
Marius Mikučionis with
Kim G. Larsen, Brian Nielsen, Shuhao Li,
Arne Skou, Anders Hessel, Paul Pettersson
1
Overview

Basic Concepts about Testing
Conformance for Real-Time Systems

Off-line Test Generation



Controllable Timed Automata
Observable Timed Automata

On-line Test Generation

Uppaal TRON tutorial
CLASSIC
CLASSIC CORA
CORA
TIGA
TIGA
TRON
TRON
2
Testing is...




... (almost) never complete:


Formal proofs deal with abstractions and leave out details.
Types of testing:


Tests can only show presence of faults but never their absence
(E. Dijkstra)
... complementary to formal verification:


an experiment (empyrical activity)
with a real object (implementation under test or IUT)
with a goal of determining it's qualities
White box, black box, functional, non-functional...
Levels of testing:

Function, component, module, integration, system
3
Error, Fault, Failure, Issue
Customer
Requirements
Tester
Developer
Implementation
Test
Pass
Error
Fault
Failure
Manager
Issue
4
Testing in practice...

Primary validation technique used in industry
• In general avg. 10-20 errors per 1000 LOC
• 30-50 % of development time and cost in embedded software



Used to:
 find errors
 determine risk of release
Part of system development life-cycle
Expensive: tedious, error prone, time consuming
5
V development model
Requirements
Acceptance
test
System
test
System
design
Integration
test
Architecture
design
Detailed
Design
Coding
Unit
test
Compiling
Implementation
6
Testing Activities
Object
(under test)
Creation (setup and procedure)
Execution (experiment run)
Evaluation (verdict assignment)
Validation (was test good?)
Pass / Fail
Inconclusive
Diagnostics
Fault location
Hypothesis
(requirements)

Usually one testing solutions covers just a few activities, e.g.:
Creation may encode verdict based on possible executions
 Execution may result in coverage profile for validation
 Execution and evaluation result in monitoring (passive testing)
 Validation may require executing and evaluating tests on faulty objects

7
Current development trends


The key to success is automation
Automation means implementable tools:


elementary steps, precise, unambiguous,
terminating...
Answer: (formal-)model-based development:





Requirement specification is a model
Test generation from a model
Test execution concurrently with a model
Test evaluation against a model
Test validation by decorating a model/IUT
8
Uppaal as Modeling Engine

Timed automata are:

Well defined: unambiguous, formal semantics

Expressive: cover large class of systems



Simple: most analysis are decidable
Abstract: allows almost any level of detail
Uppaal provides
 Practical language extensions


Fast algorithms
Compact data structures
9
Conformance Testing







Correctness is defined via conformance relation
Mostly system level: isolation is important
Black-box: state is not observable directly
Functional: value of response should be correct
Behavioral: input/output sequences
Real-time: timing is as important as computed value
Environment assumptions are explicit
Environment
Input
Output
System
Under Test
10
Real-time Model-Based Testing
Plant
Controller Program
Continuous
Discrete
sensors
actuators
Conforms-to?
Test generation
(offline or
online) wrt.
Design Model
a
b
inputs
1
2
3
4
c
a
b
outputs
c
1
3
2
1
2
3
4
1
2
3
4
a
4
UPPAAL Model
b
c
11
Conformance Relation
Specification
Implementation
give?
coin?
coin?
give?
coin?
give?





Timed Automata with Timed-LTS semantics
Input actions (?) are controlled by the environment
Output actions (!) are controlled by the implementation
Implementations are input enabled
Testing hypothesis: IUT can be modeled by some
(unknown) TA
12
Does In conform-to S1 ?
S1
I1
I6
I2
I7
I4
I3
I5
I8
?
13
Timed Conformance
 Derived from Tretman’s IOCO
 Let I, S be timed I/O LTS, P a set of states
 TTr(P): the set of timed traces from P
eg.: σ = coin?.5.req?.2.thinCoffee!.9.coin?
l2
 Out(P after σ) = possible outputs and delays after
eg. out ({l2,x=1}): {thinCoffee, 0...2}
σ
I rt-ioco S =def
 ∀σ ∈ TTr(S): Out(I after σ ) ⊆ Out(S after σ )
 TTr(I) ⊆ TTr(S) if s and I are input enabled
 Intuition
 no illegal output is produced and
 required output is produced (at right time)
See also [Krichen&Tripakis, Khoumsi] and [Briones ’07]
14
Off-Line Test Generation
Controllable
Timed Automata
15
Model Based Conformance Testing
Model
DBLclick!
x>=2 click?
x:=0
click?
x<2
Test suite
Test
Test
Test
Test
GeneGeneGenerator
Generator
rator
rator
tool
tool
tool
tool
Selection &
optimization
Implementation Relation
pass
Test
Test
execution
execution
tool
tool
Event mapping
fail
Driver
Impleme
ntat
ion
Under
Test
Does the behavior of the (blackbox)
implementation comply to that of the specification?
16
Test generation using model-checking
System model
myProtocol.xml
Trace
(witness)
Uppaal ModelChecker
Test purpose
Property
•Some
•Random
•Shortest
•Fastest
E<> connection.Established
testConnectionEst.trc
Use trace scenario as test case??!!
17
Controllable Timed Automata
Input Enabled:
all inputs can always be accepted.
Assumption about
model of SUT
Output Urgent:
enabled outputs will occur immediately.
Determinism:
two transitions with same input/output leads to the same state.
Isolated Outputs:
if an output is enabled, no other output is enabled.
18
Example
Light Controller
19
Off-Line Testing
= Optimal Reachability
transition covered
 Specific
Specific Test
Test Purposes
Purposes
 Model
Model Coverage
Coverage
 Optimal
Optimal test-suites
test-suites
20
Off-Line Testing
= Optimal Reachability
Fastest Transition Coverage =12600 ms
transition covered
out(IGrasp);
silence(200);
out(IRelease);
in(OSetLevel,0);
out(IGrasp); //@200
silence(200);
out(IRelease);//touch
in(OSetLevel,0);
//9
out(IGrasp); //@400
silence(500); //hold
in(OSetLevel,0);
out(IRelease);
//touch:switch light on
// touch: switch light off
//Bring dimmer from ActiveUp
//To Passive DN (level=0)
Page 1
//13
out(IGrasp); //@900
// Bring dimmer PassiveDn->ActiveDN->
silence(500);//hold
// ActiveUP+increase to level 10
silence(1000); in(OSetLevel,1);
silence(1000); in(OSetLevel,2);
silence(1000); in(OSetLevel,3);
silence(1000); in(OSetLevel,4);
silence(1000); in(OSetLevel,5);
silence(1000); in(OSetLevel,6);
silence(1000); in(OSetLevel,7);
silence(1000); in(OSetLevel,8);
silence(1000); in(OSetLevel,9);
silence(1000); in(OSetLevel,10
silence(1000); in(OSetLevel,9); //bring dimm State to ActiveDN
out(IRelease);
//check release->grasp is ignored
out(IGrasp); //@12400
out(IRelease);
silence(dfTolerance);
Page 2
21
Off-Line Testing
= Optimal Reachability
1W
50W
transition covered
100W
1W
 Specific
Specific Test
Test Purposes
Purposes
 Model
Model Coverage
Coverage
 Optimal
Optimal test-suites
test-suites
22
Timed Automata
(E)FSM+clocks+guards+resets
T_sw=4
T_idle=20
WANT: if touch is issued twice quickly
then the light will get brighter; otherwise the light is
turned off.
Solution: Add real-valued clock x
23
Timed Tests
T_sw=4
T_idle=20
EXAMPLE test cases
0·touch!·0·dim?·2·touch!·0·bright?·2·touch!·off?·PASS
0·touch!·0.dim?·2½·touch!·0·bright?·3·touch!·off?·PASS
0·touch!·0·dim?·5touch!·0·off?·PASS
0·touch!·0·dim?·5·touch!·0·off?·50·touch!·0·bright?·6·touch!·0·dim?·PASS
INFINITELY MANY SEQUENCES!!!!!!
24
Optimal Tests
T_sw=4
T_idle=20
1W
50W
100W
•Shortest test for bright light??
•Fastest test for bright light??
•Fastest edge-covering test suite??
•Least power consuming test??
25
Simple Light Controller
Environment model
System model
T_react=2
T_sw=4
T_idle=20
26
Test Purposes
A specific test objective (or observation) the tester wants to
make on SUT
Environment model
System model
T_react=2
T_sw=4
T_idle=20
TP1: Check that the light can become bright:
E<> LightController.bright
•Shortest Test: 20·touch!·0·bright?·PASS
•Fastest Test: 0·touch!·0·dim?·2·touch!·0·bright ?·PASS
27
Test Purposes 2
Environment model*TP2
System model
T_react=2
T_sw=4
T_idle=20
TP2: Check that the light switches off after three successive
touches
Use restricted environment and E<> tpEnv.goal
•The fastest test sequence is
0·touch!·0·dim?·2·touch!·0·bright?·2·touch!·0·off?·PASS
28
Coverage Based Test Generation



Multi purpose testing
Cover measurement
Examples:



l1
c!
Location coverage,
Edge coverage,
l
Definition/use pair coverage
a? x:=0
b!
l2
a?
x≥2
x<2
4
l3
29
Coverage Based Test Generation



Multi purpose testing
Cover measurement
Examples:



l1
c!
Location coverage,
Edge coverage,
l
Definition/use pair coverage
a? x:=0
b!
l2
a?
x≥2
x<2
4
l3
30
Coverage Based Test Generation



Multi purpose testing
Cover measurement
Examples:



l1
c!
Location coverage,
Edge coverage,
l
Definition/use pair coverage
a? x:=0
b!
l2
a?
x≥2
x<2
4
l3
31
Coverage Based Test Generation



Multi purpose testing
Cover measurement
Examples:



l1
c!
Location coverage,
Edge coverage,
l
Definition/use pair coverage
a? x:=0
b!
l2
x≥2
x<2
4
l3
32
Coverage Based Test Generation



Multi purpose testing
Cover measurement
Examples:





Locations coverage,
Edge coverage,
Definition/use pair coverage
All Definition/Use pairs
l1
a? x:=0
b!
l2
a?
x≥2
c!
l4
x<2
l3
Generated by min-cost reachability analysis of
annotated graph
33
Location Coverage



Test sequence traversing all locations
Encoding:

Enumerate locations l0,…,ln

Add an auxiliary variable li for each location

Label each ingoing edge to location i li:=true

Mark initial visited l0:=true
Check: EF( l0=true ∧ … ∧ ln=true )
lj:=true
lj
lj:=true
34
Edge Coverage



Test sequence traversing all edges
Encoding:

Enumerate edges e0,…,en

Add auxiliary variable ei for each edge

Label each edge ei:=true
Check: EF( e0=true ∧ … ∧ en=true )
a? x:=0 e0:=1
l1
c!
e4:=1
l4
x≥2
b! e1:=1
x<2
e3:=1
l2
a? e2:=1
l3
35
Edge Coverage
EC: T_react=0 0·touch!·0·dim?·0·touch!·0·bright?·0·touch!
·0·off?·
20·touch!·0·bright?·4·touch!·0·dim?·4·touch!·0·off?·PASS
Time=28
EC': T_react=2
0·touch!·0·dim?·4·touch!·0·off?· 20·touch!·0·bright?·
4·touch!·0·dim?·2·touch!·0·bright?·2·touch!·0·off?·PASS
Time=32
EC'': pausing user T_react=2, T_pause=5
0·touch!·0·dim?·2·touch!·0·bright?·5·touch!·0·dim?·
4·touch!·0·off?·20·touch!·0·bright?·2·touch!·0·off?·PASS
Time=33
36
Definition/Use Pair Coverage


Dataflow coverage technique
Def/use pair of variable x:
x:=0
definition

...
no defs
x≥ 4
use
Encoding:




vd ∈ { false} ∪{ e0, …, en }, initially false
Boolean array du of size |E| x |E|
At definition on edge i: vd:=ei
At use on edge j: if( vd ) then du[vd,ej]:=true
.
.
37
Definition/Use Pair Coverage


Dataflow coverage technique
Def/use pair of variable x:
x:=0
definition

no defs



du: 0
0
n-1
use
Encoding:


...
x≥ 4
vd ∈ { false} ∪{ e0, …, en }, initially false
Boolean array du of size |E| x |E|
At definition on edge i: vd:=ei
i
n-1
j
At use on edge j: if( vd ) then du[vd,ej]:=true
Check:

EF( all du[i,j] = true )
38
Uppaal CoVer by Anders Hessel and Paul Pettersson



Generates coverage-optimal test-suites:
Uses models with deterministic IUT and non-deterministic
environment.
Provides a language for specifying coverage:





locations, edges, variable definition-use
Internally generates corresponding observer automata.
Uses observer automata states to encode the state of coverage.
=> automatic model decoration, better control over model,
dynamic (more efficient) memory usage
Applied on Wireless Application Protocol gateway.
39
Test Suite Generation


In general a set of test cases is needed to cover a test criteria
Add global reset of SUT and environment model and associate a
cost (of system reset)
R
initial
x=C
x:=0
x≤ C
reset?
reset

Same encodings and min-cost reachability

Test sequence σ = ε0,i0,…,ε1, i1, reset ε2,i2, …,ε0,i0,reset,ε1, i1,ε2,i2,…

Test suite T = {σ1, …, σn } with
minimum cost
σi
40
The Philips Audio Protocol

A bus based protocol for exchanging control messages
between audio components


Collisions
Tolerance on timing events
Bit stream 1
Manchester encoding
0
0
0
1
1
0
isUP
up dn
in0
TX
in0 in1empty
RX
coll
out0 out1
end
TX RX
41
Philips Audio Protocol
42
Benchmark Example

Philips Audio Protocol
43
Off-Line Test Generation
Observable Timed Automata
44
Observable Timed Automata




Determinism:
two transitions with same input/output leads to the
same state
Input Enabled:
all inputs can always be accepted
Time Uncertainty of outputs:
timing of outputs uncontrollable by tester
Uncontrollable output:
IUT controls which enabled output will occur in what
order
45
Timed Games and Testing
Tidle=20
Tsw=4
Off-line test-case generation =
Compute winning strategy for reaching Bright
Assign verdicts st. lost game means IUT not conforming
46
A trick light control
Tidle=20
Tsw=4
How to test for Bright ?
E<> (control: A<> Bright)
or
<<c,u>>
} (<<c>> }
Bright)
47
Cooperative Strategies
Model Statespace
possibly winning
initial
winning
goal
loosing
• Play the game (execute test) while time available or game is lost
• Possibly using ranomized online testing
48
On-Line Testing
emulation, execution and evaluation
49
50
Automated Model Based Conformance Testing
Model
Test suite
DBLclick!
x>=2 click?
x:=0
click?
x<2
Test
Test
Test
Test
GeneGeneGenerator
Generator
rator
rator
tool
tool
tool
tool
pass
Test
Test
execution
execution
tool
tool
fail
Adaptor
Selection &
optimization
Correctness Relation
Impleme
ntat
ion
Under
Test
Does the behavior of the (blackbox)
implementation comply to that of the specification?
51
Online Testing
Model
DBLclick!
x>=2 click?
x:=0
click?
x<2
pass
Test
Test
Test
Test
GeneGeneGenerator
Generator
rator
rator
tool
tool
tool
tool
input
output
Test
Test
execution
execution
tool
tool
Adaptor
fail
Selection &
optimization
Correctness Relation
•Test generated and executed eventby-event (randomly)
Impleme
ntation
Under
Test
•A.K.A on-the-fly testing
52
Implementation relation
Relativized real-time io-conformance
E
Environment
assumptions
ε0,i0,ε1,i1…
ε0’ ,o0,ε1’ ,o1…
S
I
System
Model
IUT
•E,S, I are input enabled Timed LTS
•Let P be a set of states
•TTr(P): the set of timed traces from states in P
•P after σ = the set of states reachable after timed trace σ
•Out(P) = possible outputs and delays from states in P
•I rt-iocoE S =def
∀σ ∈ TTr(E): Out((E,I) after σ) ⊆ Out((E,S) after σ)
•I rt-iocoE s iff TTr(I) ∩ TTr(E) ⊆ TTr(S) ∩ TTr(E) // input enabled
•Intuition, for all assumed environment behaviors, the IUT
•never produces illegal output, and
•always produces required output in time
53
Sample Cooling Controller
Env-model
IUT-model
Cr
On!
Off!
Low?
Med?
High?
•When T is high (low) switch on (off) cooling within r secs.
•When T is medium cooling may be either on or off (impl freedom)
54
Environment Modeling
Temp.
EM Any
action possible at any time
E1 Only realistic temperature variations
E2 Temperature never increases when cooling
EL No inputs (completely passive)
High!
Med!
Low!
time
EM
E1
EL
EL
E2
E1
E2
EM
55
Re-use Testing Effort


1.
Given I, E, S
Assume I rt-iocoE S
Given new (weaker) system specification S’
If S
2.
S’ then I rt-iocoE S’
Given new (stronger) environment specification E’
If E’
E then I rt-iocoE’ S
56
Online Testing Algorithm
57
Algorithm Idea:

State-set tracking
Dynamically compute all potential states that the model
M can reach after the timed trace ε0,i0,ε1,o1,ε2,i2,o2,…
[Tripakis] Failure Diagnosis

Z=M after (ε0,i0,ε1,o1,ε2,i2,o2)

If Z= ∅ the IUT has made a computation not in model: FAIL

i is a relevant input in Env iff I 2 EnvOutput(Z)
58
Online State Estimation
Timed Automata
Specification
State-set explorer:
maintain and analyse a set of symbolic states in
real time!
Z4
Z1Z1 Z
5 3
Z17Z1
Z7
Z 0
8
Z16 1Z4 Z
Z2ZZ18 Z9
Z6 12
Z15
i!
2.75
O?
System
Under
Test
59
(Abstract) Online Algorithm
Algorithm TestGenExe (S, E, IUT, T ) returns {pass, fail)
Z := {(s0, e0)}.
while Z ≠ ∅ and ♯iterations ≤ T do either randomly:
1. // offer an input
if EnvOutput(Z) ≠ ∅
randomly choose i2 EnvOutput(Z)
send i to IUT
Z := Z After i
1. // wait d for an output
randomly choose d2 Delays(Z)
wait (for d time units or output o at d′ ≤ d)
if o occurred then
Z := Z After d′
Z := Z After o // may become ∅ (⇒fail)
else
Z := Z After d // no output within d delay
3. restart:
Z := {(s0, e0)}, reset IUT //reset and restart
if Z = ∅ then return fail else return pass
60
(Abstract) Online Algorithm
Algorithm TestGenExe (S, E, IUT, T ) returns {pass, fail)
Z := {(s0, e0)}.
while Z ≠ ∅ ∧ ♯iterations ≤ T do either randomly:
1. // offer an input
if EnvOutput(Z) ≠ ∅
randomly choose i ∈ EnvOutput(Z)
send i to IUT
Z := Z After i •Sound (fail => non-conforming)
1. // wait d for an output
•Complete (non-conforming =>
randomly choose dfail
∈Delays(Z)
as T → ∞, (under some
wait (for d time units
or output
o at d′ ≤ d)
technical
assumptions))
if o occurred then
Z := Z After d′
Z := Z After o // may become ∅ (⇒fail)
else
Z := Z After d // no output within d delay
3. restart:
Z := {(s0, e0)}, reset IUT //reset and restart
if Z = ∅ then return fail else return pass
61
State-set Operations
Z after a: possible states
after action a (and τ*)
Z
τ τ
a τ →→
Z after ε :possible states
after τ* and εi , totaling a delay of ε
Z
1 τ
→
→→
→ →→
→→→→
a
→ →τ τ
→ →τ
→→→→
2
→ →τ 1
→ →2
a τ τ τ
τ τ τ 5
ε

4 τ
(5)
time
Can be computed efficiently using the symbolic
data structures and algorithms in Uppaal
62
Online Testing Example
63
Online Testing
64
Online Testing
65
Online Testing
66
Online Testing
67
Online Testing
68
Online Testing
69
Online Testing
70
Online Testing
71
Online Testing
72
Online Testing
73
Online Testing
74
Online Testing
75
DEMO Touch-sensitive Light-Controller
∞
•Patient user: Wait=
•Impatient: Wait=15
76
Test Setup
mousePress
mouseRelease
TRON
Testing
Host
tcp/ip
•Real-time
•Simulated time
Test
Fixture
setLevel
LightControllerGUI
grasp
release
grasp
setLevel release
LightController
JavaVM+w2k/Linux
77
Mutants

Mutant: Non-conforming program version with a seeded
error
synchronized implements
public void handleTouch()
switch
• M1 incorrectly
if(lightState==lightOff) {
{
setLevel(oldLevel);
lightState=lightOn;
}
else { //was missing
if(lightState==lightOn){
oldLevel=level;
setLevel(0);
lightState=lightOff;
}

M2 violates a deadline
78
Industrial Cooling Plants
79
Industrial Application:
Danfoss Electronic Cooling Controller
Sensor Input
•air temperature sensor
•defrost temperature sensor
•(door open sensor)
Keypad Input
•2 buttons (~40 user settable
parameters)
Output Relays
•compressor relay
•defrost relay
•alarm relay
•(fan relay)
Display Output
•alarm / error indication
•mode indication
•current calculated temperature
•Optional real-time clock or LON network module
80
Industrial Application:
Danfoss Electronic Cooling Controller
Sensor Input
•air temperature sensor
•defrost temperature sensor
•(door open sensor)
Keypad Input
•2 buttons (~40 user settable
parameters)
Output Relays
•compressor relay
•defrost relay
•alarm relay
•(fan relay)
Display Output
•alarm / error indication
•mode indication
•current calculated temperature
•Optional real-time clock or LON network module
81
Example Test Run
(log visualization)
3800
3700
3600
3500
3400
3300
3200
3100
3000
2900
2800
2700
2600
2500
2400
2300
2200
2100
2000
1900
1800
1700
1600
1500
setTemp
modelTemp
ekcTemp
CON
COFF
AON
AOFF
alarmRst
HADOn
HADOff
DON
DOFF
manDefrostOn
manDefrostOff
0
100000
200000
defrostOff?
compressorOn!
300000
400000
resetAlarm?
AOFF!
500000
600000
700000
800000
900000
//defrost complete
DOFF!
CON!
HighAlarmDisplayOff!
alarmOn!
alarmDisplayOn!
manualDefrostOn?
COFF!
DON!
82
Model-based
Testing
of
Real Time Systems
Conclusions
83
Conclusions



Testing real-time systems is theoretically and
practically challenging
Promising techniques and tools
Explicit environment modeling






Realism and guiding
Separation of concerns
Modularity
Creative tool uses
Theoretical properties
Real-time online testing from timed automata is
feasible, but

Many open research issues
84
Research Problems











Testing Theory
Timed games with partial observability
Hybrid extensions
Other Quantitative Properties
Probabilistic Extensions, Performance testing
Efficient data structures and algorithms for state set
computation
Diagnosis & Debugging
Guiding and Coverage Measurement
Real-Time execution of TRON
Adapter Abstraction, IUT clock synchronization
Further Industrial Cases
85
Related Work

Formal Testing Frameworks


Real-Time Implementation Relations


[Dill’89, Larsen’97,…]
Online state-set computation


[Khoumsi’03, Briones’04, Krichen’04]
Symbolic Reachability analysis of Timed Automata


[Brinksma, Tretmans]
[Tripakis’02]
Online Testing

[Tretmans’99, Peleska’02, Krichen’04]
86
Uppaal TRON Tutorial
modeling, implementing and testing
87
Test the setup







Check Java version by “java -version”
 Should be Sun Java 6 or 5
Check ant version by “ant -version”
 Should be 1.7.0 or 1.7.1
Unpack (copy) Uppaal TRON 1.5 distribution
Go to “java” directory of Uppaal TRON distribution
Recompile:
 “ant clean jar”
Run test of smartlamp:
 Linux: “start-light-v.sh & start-test-v.sh”
 Windows: “start-test-v.bat”
Try commands from Makefile (Linux only):
 “make test-light-s”
 “make test-dummy-s”
88
Task: model, implement, test

Simple shutter controller for photo camera:
 When user presses “configure” sensors are read:
 luminance (L): 10^0 – 10^5 lux
 aperture (A): 1.41, 2, 2.83, 4, 5.66, 8, 11.31, 16, 22.63, 32
 focal length (F): 0.05m
 Controller then computes exposition (E): 1ms - 2s
 E=3.14*(10^2)*((F/2*A)^2)/L (in seconds)
 When user presses “shoot”:
 Shutter should get signal “open” within 1ms
 Shutter should remain open for at least E-0.1ms time
 Shutter should get signal “close” within E time after “open”
configure(L, A, F), shoot
User
Controller
open,
close
Shutter
89
Test Specification

Run tests at least against three environments:

Human behavior:



Slow user, use clock guards to slow down user
All tests should pass
Extreme but still realistic behavior:


Fast user, use clock invariants to force more inputs
Test may fail:



Find out why test fail
Advanced: find boundary conditions that test does not fail.
Unrestricted:


Allow any input at any time
It is OK for tests to fail, explain why tests fail.
90
Tips for Modeling



The model consists of a closed system:
 All sending and receiving synchronizations are
paired: for every sender there is a receiver.
Model is partitioned into:
 Processes for environment
 Processes for implementation
 All communication between env. and IUT goes
only with observable channel synchronization
 Adapter processes belong to implementation
Use “tron -i dot” option to get signal flow diagram
91
Model partition example

tron -v 3 -i dot fridge.xml < fridge.trn | dot -Tpng -o fridge.png

Where fridge.trn contains:
input temp(T);
output turn_on(), turn_off();
precision 1000; // micro-sec.
timeout 10000; // mtu
92
Input Enabledness



IUT model should be input enabled:
 If not, diagnostics might be misleading
Environment model should be input enabled:
 If not, there might be “Inconclusive” verdicts
Use loop edges with caution when consuming
redundant observable actions
93
Tips for Programming in Java

Use dummy example as a stub in java dir:
see src/com/uppaal/dummy/Dummy.java
 execute() method is the implementation code

DummyInterface.java declares inputs
 DummyListener.java declares outputs
 TestIOHandler.java handles the communication:

configure(Reporter) registers observable channels
 run() translates tester's input messages to Dummy calls
 reportMyOutput() translates calls into output messages to tester

94
Thread programming

Monitor synchronization:
Producer:
…
lock.lock();
queue.add(item);
cond.signalAll();
lock.unlock();
...





Consumer:
…
lock.lock()
while (queue.isEmpty())
cond.await();
queue.remove();
lock.unlock();
...
Consumer and producer share queue
queue is protected by lock
Consumer blocks and releases lock in await if queue is empty
cond is associated and surrounded with lock
cond wakes consumer up which reacquires lock and continues
95
Testing using Uppaal TRON

TRON can be run in:



Real-world-time (requires adapter models, see smartlamp)
Virtual time (provides “lab-conditions” and releases from
scheduling and communication latency problems)
Virtual time (option “-Q”):






Uses single virtual clock
All threads are registered at this clock (use VirtualThread instead
of Thread)
All time-related calls are forwarded to this clock
Virtual clock is incremented only when all threads agree to wait
May deadlock if at least one thread misbehaves
Possible Zeno behavior (time does not progress)
96
Tips for running online tests

If test fails and diagnostics at the end is not enough:
 Inspect the last good state set provided by TRON:

Validate model:



Would you expect such state to be reachable?
No? How such state can be reached? Use UPPAAL verifier to find out.
Would/did implementation do as the model? Why not?
Add “System.out.print” in your implementation
 Ask TRON for more verbose messages:

add “-D test.log” option to save test trace to test.log
 use “-v 10” instead of “-v 9” to see engine events


If test passes unexpectedly (e.g. TRON is too passive):
 Use “-P” option with larger/smaller intervals,
or set to “-P random”
97
More Details

Options are documented in the user manual
http://www.cs.aau.dk/~marius/tron/manual.pdf

When all else fail...



See commands in Makefile rules
See smartlamp example source code
Write an email to: [email protected]
98
Thanks for your
attention!