Verification and Test Automation of
UML Projects
Nikita Voinov, Vsevolod Kotlyarov
(Saint-Petersburg State Polytechnic University)
The Third Spring Young Researchers Colloquium on
Software Engineering
Moscow
May 28-29
2009
Software Quality Assurance
• Unambiguity of requirements
Solution:
usage of formal languages and notations (UML – Unified Modeling
Language)
• Software functionality’s correctness checking
Solution:
– verification
– testing
2
SYRCoSE 2009
Issues
• Model of the system on some
formal language shall be
created for verification
• Manual testing
Long and laborious
processes
• Lack of technologies which allow to integrate testing
and verification
3
SYRCoSE 2009
Proposed Solution
Initial Requirements
(UML)
correction of
requirements
automated process
of formalization
Verification
(VRS)
automated process
of tests generation
Testing
(TAT)
TTCN
(Testing
and Test
Control
Notation)
4
SYRCoSE 2009
Basic Protocol –
a simple MSC diagram, which specifies:
• the state of the system where the system shall perform
some activity – pre-condition
• the activity itself (transmission of a message or
performance of an action) – process part
• the state of the system after the activity is performed –
post-condition
pre-condition
process part
action
message
post-condition
5
SYRCoSE 2009
VRS (Verification of Requirement
Specifications)
• combines model checking with deductive verification
• checking the properties of requirements represented
with basic protocols
• detection of non-deterministic behavior,
unreachability of specified states, deadlocks
• criterion of requirement’s satisfiability in VRS is
existence of sequence of required events (actions,
signals) contained in basic protocols in definite
order; such sequence is called “trace”
6
SYRCoSE 2009
Conversion of a Fragment of UML
SM Diagram into a Basic Protocol
Special VRS
module “uml2bp”
is used for
autoformalization
7
SYRCoSE 2009
Verification Stage
• Step 1. Formulation of filters and heuristics for the current
project. They help to decrease number of traces by pointing
the trace generator to the definite direction.
• Step 2. Performing an automatic trace generation cycle.
• Step 3. Analysis of findings with deadlocks, inconsistency
and other issues. Correcting the generated basic protocols
or initial requirements. Repeat steps 1-3.
• Step 4. Analysis of generated traces with a script to check
whether the coverage criteria are satisfied. Repeat steps 1-4
if needed.
8
SYRCoSE 2009
Sample State Machine Diagram
9
SYRCoSE 2009
Graph with All States without
Detailed Behavior
10
SYRCoSE 2009
Graph with All States with Detailed
Behavior of ‘Suspended’ State
UDI_LDI
Suspended
Start
UEA
UEI_LEI
11
SYRCoSE 2009
Trace for the Graph with All States
12
SYRCoSE 2009
Trace for the Graph with Detailed
Behavior of ‘Suspended’ State
13
SYRCoSE 2009
Traces Merging (Glue In)
14
SYRCoSE 2009
TAT (Test Automation Toolset)
• templates for generation of tests in C, Java, TTCN
languages
• automated testing cycle based on user-defined
scenarios developed in formal language MSC
• customizable for different platforms with different
environments
15
SYRCoSE 2009
Overall Scheme of Automatic TTCN
Tests Generation
UML diagram
16
SYRCoSE 2009
Adding Values to MSC
Input: MSC with parameters
Output: MSC with values
Configuration items: .xls file with parameters values; VB script for xls-> txt conversion;
add_values.tcl (script)
Notes: the script finds identical parameters names in MSC and .xls file and replaces them in
MSC by values in .xls.
.xls file with parameters values :
MSC with values :
17
SYRCoSE 2009
TTCN Test Cases Generation
TTCN test case:
File for test cases launch:
18
SYRCoSE 2009
Results of Piloting in Telecom
Project
• autoformalization stage: about 4000 basic protocols
were generated in 3 minutes (while manual efforts are
estimated in 10-50 basic protocols per day)
• verification stage: about 100 findings were
discovered, 12 of them were considered defects and
fixed in future versions of the product
• tests generation stage:
Time Efforts
250
Time, min
200
150
manual
100
50
automated
0
0
SYRCoSE 2009
5
10
15
Number of Tests
20
25
19
Novelty of Work
• automated conversion of UML specifications into formal
model in the language of basic protocols
• methodic of large-scale models analysis using VRS
technology
• new TAT template for generation of tests in TTCN
language
20
SYRCoSE 2009
THANK YOU
21
SYRCoSE 2009
Descargar

Presentation title goes here and breaks like this.