Testing at RadBoud
Lars Frantzen, Pieter Koopman, René de Vries,
Tim Willemse, Jan Tretmans
Radboud University
Nijmegen
©
Jan Tretmans Radboud University Nijmegen
1
Testing Research in Nijmegen
Overview
©
 Introduction
Jan Tretmans
 Integrating Data with ioco
Lars Frantzen
 Specification Mining
Tim Willemse
Jan Tretmans Radboud University Nijmegen
2
Model Based Testing
with Transition Systems
gentest
: LTS
generation

(TTS)
tool
s spec
 LTS
i
IUT confto
i ioco spec
s
exhaustive
  sound
test
test
execution
t ||
tooli
tool
IUT
confto
ioco
s
spec
i IUT
 IOTS
IUT
i || passes
der(s) tests
 pass
©
Jan Tretmans Radboud University Nijmegen
pass fail
3
A Tool for Transition Systems
Testing: TorX
 On-the-fly test generation and test execution
 Implementation relation: ioco
 Mainly applicable to reactive systems / state based systems;
 specification languages: LOTOS, Promela, FSP, Automata
user:
manual
automatic
next
input
specification
check
output
offer
input
TorX
observe
output
IUT
pass
fail
inconclusive
©
Jan Tretmans Radboud University Nijmegen
4
Testing Transition Systems: Extensions
Status
model
with data
and time
and hybrid
and action
refinement
test case
?coin1
?coin2
? money  n: int 
! money
?coin3
?
[ n  35 ] ->
[ n  50 ] ->
? button1
? button2
:= 00
c
Vt:=:=00 Vcc :=
d Vct </10
dt =
3
! button2
d Vcc</15
dt =
[Vt = 15 ] ->
! tea
2
[[V
c c =510
] ->] ->
! coffee
? coffee
? tea
pass
©
Jan Tretmans Radboud University Nijmegen

fai
l
fai
l
5
Testing Properties
of Input/Output Programs: Gst
x: real
IUT
pre: x 0
i(x) = x
 Specification: property over x and y
 property(x,y) = x  0  |y  y - x| 
y: real
post: |y  y - x| 


 Implementation is function i :: X  Y
 Test set T  X
 A tool like GST (or QuickCheck) generates thousands of tests
by systematic traversal of all values of type X
 But still: what is a "good" set ?
©
Jan Tretmans Radboud University Nijmegen
6
Current and Future Research
Radboud
 Testing transition systems with data
 integrating data with ioco
 Specification mining
 reverse engineering of specification from observations
 Approximate correctness
 some systems are more correct than others
 test selection
 Gst
 specification/model testing
 Model Based Testing with UML
 use of industrial modelling techniques
 Integration of real-time and data testing
©
Jan Tretmans Radboud University Nijmegen
7
Current and Future Research
Radboud
 Tools for transition system testing
 TorX
 generic test environments
 automatic generation of test adapter and test interface
 TorXakis - experimenting with data/symbolic testing
 Applications
©
 web page testing
Gst
 smart card testing
Gst / TorX(akis)
 ASML DCB (Laser Dose Control)
TorX
Jan Tretmans Radboud University Nijmegen
8
Testing Projects
 Atomyste
- ATOm splitting in eMbedded sYStem TEsting
Uni. of Twente
Radboud Uni. Nijmegen
 Stress
- Systematic Testing of Real-time Embedded Software Systems
Uni. of Twente
 Tangram
Radboud Uni. Nijmegen
- Model Based Testing and Diagnosis
ASML, ESI, TUD, TUE, UT, RU, S&T, TNO
 Tarot
- EU FP6 Marie Curie
 Artist 2
©
- EU FP6 Network of Excellence
Jan Tretmans Radboud University Nijmegen
9
Descargar

Automated Model Based Testing From Theory via Tools to