Sequence Chart Studio
(SCStudio)
Mat´uˇs Madzin, Adrian Farmadin
Faculty of Informatics, Masaryk University
October 24, 2012
1 / 28
Sequence Chart Studio
provides verification and validation algorithms
well arranged output
2 / 28
Sequence Chart Studio
provides verification and validation algorithms
well arranged output
supports Message Sequence Chart (MSC) formalism
open source verification tool (plug-in to Microsoft Visio)
user-friendly graphical and textual interfaces
2 / 28
Graphical User Interface
3 / 28
Basic MSC
Basic Message Sequence Charts (BMSC) diagrams are used to
describe a communication among instances.
4 / 28
Basic MSC
Basic Message Sequence Charts (BMSC) diagrams are used to
describe a communication among instances.
Instance – object which can communicate
Event – send or receive a message
Coregion – area without event ordering
4 / 28
BMSC Example
Obr.: BMSC
5 / 28
High-level MSC
High-level Message Sequence Charts (HMSC) diagrams are graphs
which allow user to model a communication in hierarchical
structure. HMSC with depth 1 is also called MSC graph.
6 / 28
High-level MSC
High-level Message Sequence Charts (HMSC) diagrams are graphs
which allow user to model a communication in hierarchical
structure. HMSC with depth 1 is also called MSC graph.
Start Node – beginning of the communication
Reference Node – high-level representation of some MSC diagram
End Node – ending of the communication
6 / 28
HMSC Example
Obr.: HMSC
7 / 28
Beautify Transformer
Beautify transformer redraws a diagram into well-arranged form.
8 / 28
Beautify Transformer
Beautify transformer redraws a diagram into well-arranged form.
Non-well-arranged diagram
8 / 28
Beautify Transformer
Beautify transformer redraws a diagram into well-arranged form.
Non-well-arranged diagram Well-arranged diagram
8 / 28
Protocol Design
Designers create a communication protocol:
9 / 28
Protocol Verification
Verification tools identify a race condition problem.
10 / 28
Tighten Time
Tighten Time transformer restricts time intervals to minimal ranges
11 / 28
Tighten Time
Tighten Time transformer restricts time intervals to minimal ranges
11 / 28
Time Consistency
Time Consistency checker finds intervals which are in a conflict
with others
12 / 28
Time Consistency
Time Consistency checker finds intervals which are in a conflict
with others
12 / 28
Find Flow
Find Flow function checks whether a basic MSC is contained in
another MSC diagram.
Specification
13 / 28
Find Flow
Find Flow function checks whether a basic MSC is contained in
another MSC diagram.
Specification Flow
13 / 28
Find Flow
Find Flow function checks whether a basic MSC is contained in
another MSC diagram.
Specification Find Flow result
13 / 28
Time Constraints in Find Flow
Find Flow supports
diagrams with time constraints
Hierarchical MSC (HMSC) diagrams
14 / 28
Time Constraints in Find Flow
Find Flow supports
diagrams with time constraints
Hierarchical MSC (HMSC) diagrams
Specification Flow
14 / 28
Time Constraints in Find Flow
Find Flow supports
diagrams with time constraints
Hierarchical MSC (HMSC) diagrams
Specification Flow
14 / 28
Time Constraints in Find Flow
Find Flow supports
diagrams with time constraints
Hierarchical MSC (HMSC) diagrams
Find Flow result Flow
14 / 28
Time Constraints in Find Flow
Find Flow supports
diagrams with time constraints
Hierarchical MSC (HMSC) diagrams
Find Flow result Flow
14 / 28
Summary
drawing aids
easy and comfortable drawing
message flipping, shortcuts, . . .
transformers Beautify, Tighten Time, . . .
verification & validation tools
(Time) Race checker
Time Consistency checker
Strong Realizability checker
additional functions
Find Flow
Monte Carlo simulation (experimental)
15 / 28
Summary
drawing aids
easy and comfortable drawing
message flipping, shortcuts, . . .
transformers Beautify, Tighten Time, . . .
verification & validation tools
(Time) Race checker
Time Consistency checker
Strong Realizability checker
additional functions
Find Flow
Monte Carlo simulation (experimental)
15 / 28
Summary
drawing aids
easy and comfortable drawing
message flipping, shortcuts, . . .
transformers Beautify, Tighten Time, . . .
verification & validation tools
(Time) Race checker
Time Consistency checker
Strong Realizability checker
additional functions
Find Flow
Monte Carlo simulation (experimental)
SCStudio is available on sourceforge.net
15 / 28
Happenings in last year
ANF DATA spol. s.r.o.
Siemens Convergence Creators, s.r.o.
16 / 28
Happenings in last year
ANF DATA spol. s.r.o.
Siemens Convergence Creators, s.r.o.
conference ACSD’12
16 / 28
Happenings in last year
ANF DATA spol. s.r.o.
Siemens Convergence Creators, s.r.o.
conference ACSD’12
1618 downloads last year (max 159 in one month)
16 / 28
Happenings in last year
ANF DATA spol. s.r.o.
Siemens Convergence Creators, s.r.o.
conference ACSD’12
1618 downloads last year (max 159 in one month)
improved Find Flow
16 / 28
Happenings in last year
ANF DATA spol. s.r.o.
Siemens Convergence Creators, s.r.o.
conference ACSD’12
1618 downloads last year (max 159 in one month)
improved Find Flow
new students
16 / 28
Students
Export to TEX- bachelor
Import PCAP - bachelor
Time Order Visualization -bachelor
synchronize messages on instances by time stamps
Models of Open IMS -master
create formal models of Open IMS system (MSCs, Petri nets)
17 / 28
Export to TEX
Existed exports:
textual form of ITU-T standard
DiVinE (LTL model checking tool)
Target:
express diagrams in TEX source code
Motivation:
comfortable diagram’s usage in presentations
18 / 28
Assignment
Requirements
TEX source code for exact visualization from MS Visio
readable & editable code
MSC.sty
does not support all objects
weak support of object settings
19 / 28
My Work
Necessary to add:
objects: orders, comments ...
object properties
Additional targets:
colors
upload new library to CTAN
20 / 28
Example
NAME NAME NAME
NAME NAME
NAME NAME
NAME
msc Page 1
21 / 28
Source Code Example
%%%% Scale Y
\def\scale@y{1.0}
%%%% Instance first and last level height
\setlength{\firstlevelheight}{10mm*\real{\scale@y}}
\setlength{\lastlevelheight}{10mm*\real{\scale@y}}
%%%% Levels:
\def\levela{10mm*\real{\scale@y}}
\def\levelb{5mm*\real{\scale@y}}
%%%% Slope:
\def\slopea{3mm*\real{\scale@y}}
\def\slopeb{\levela+\levelb}
%%%% Instance width:
\def\instanceWidtha{10mm*\real{\scale@y}}
22 / 28
PCAP Import
Existed imports:
textual form of ITU-T standard
Target:
transform network traffic from pcap files and visualize them
as MSC diagrams
Motivation:
compare traffic flows with protocol design diagrams by Find
Flow algorithm
23 / 28
Time Order Visualization
Existed visualization:
small layout assigned according ITU-T standard
Target:
visualization with synchronize time clocks on instances
Motivation:
asked by users, specially for network traffic visualization
24 / 28
Models of Open IMS
Target:
create formal models of Open IMS system focused on SIP
protocol
Motivation:
detailed analysis helps us to apply SCStudio in real project
development
25 / 28
Future Work
Extend Find Flow to be usable on PCAP files in real networks and
cooperation with Siemens.
Targets in test area:
cover of high-level diagram
test case generation
Targets in user interaction:
GUI for Linux
improve MS Visio plug-in
26 / 28
Looking for students
Theses
Find Flow (2 - 3 bachelor students)
MS Visio stencils (1 student)
Extend ITU-T standard (1 bachelor student)
Libre Office plug-in (probably 1 student)
Formal verification of SCStudio (probably 1 student)
Local Choice decidability (1 master student)
27 / 28
Thank you for your attention
scstudio.sourceforge.net
28 / 28