Sequence Chart Studio
(SCStudio)
Martin Bezděka, Ondřej Bouda, Luboš Korenčiak, Matúš Madzin, Vojtěch Řehák
Faculty of Informatics, Masaryk University
November 8, 2012
INVESTICE DO ROZVOJE VZDĚLÁVÁNI
1/17
Problem: Late discovery of a bug is a proble
Problem: Late discovery of a bug is a problem
Why developers don't use formal verification?
Problem: Late discovery of a bug is a problem!
Why developers don't use formal verification?
Telecommunication area:
• system description done by natural language and sequence diagrams
Problem: Late discovery of a bug is a problem!
Why developers don't use formal verification?
Telecommunication area:
• system description done by natural language and sequence diagrams
• formal verification on sequence diagrams is possible but not used
Sequence Chart Studio
• supports Message Sequence Chart (MSC) formalism
3/17
Sequence Chart Studio
• supports Message Sequence Chart (MSC) formalism a user-friendly graphical and textual interfaces
3/17
Sequence Chart Studio
• supports Message Sequence Chart (MSC) formalism
• user-friendly graphical and textual interfaces
• provides verification and validation algorithms
3/17
Sequence Chart Studio
• supports Message Sequence Chart (MSC) formalism
• user-friendly graphical and textual interfaces
• provides verification and validation algorithms
• well arranged output
Message sequence chart is standardized by ITU-T. Standard specifies two equivalent MSC notations (graphical, textual).
MSC Standard
Message sequence chart is standardized by ITU-T. Standard specifies two equivalent MSC notations (graphical, textual).
Basic MSC diagrams: instances message
Drawing Aids
• automatic message/arrow snapping
• automatic drawing
• shortcuts
• drawing transformations, e.g. beautify
6/17
Beautify Transformer
Beautify transformer redraws a diagram into well-arranged form.
7/17
Beautify Transformer
Beautify transformer redraws a diagram into well-arranged form. b c a
Non-well-arranged diagram
7/17
Beautify Transformer
Beautify transformer redraws a diagram into well-arranged form.
b c a a b c
Non-well-arranged diagram Well-arranged diagram
7/17
Protocol Design
Designers create a communication protocol:
Client
Interface
Server
			
		_ Register	
	Resoonse		
	4- Request		
		---► Response	
	<--'		
8/17
Protocol Verification
Verification tools identify a race condition problem.
Client
Interface
] r——i
Server
Response
Reg iste
	--É
.4----	Response
9/17
Add Time Intervals
The race condition could be solved by adding time constraints Client Interface Server
10/17
Tighten Time
Tighten Time transformer restricts time intervals to minimal ranges
Client Interface Server
11/17
Tighten Time
Tighten Time transformer restricts time intervals to minimal ranges
Client Interface Server
11/17
Time Consistency
Time Consistency checker finds intervals which are in a confl with others
Client Interface Server
Time Consistency
Time Consistency checker finds intervals which are in a confl with others
Client Interface Server
Testing
SCStudio is able to
q transform network traffic from pcap files and visualize them as MSC diagrams
14/17
Testing
SCStudio is able to
• transform network traffic from pcap files and visualize them as MSC diagrams
• compare traffic flows with diagrams of protocol design
14/17
Find Flow function checks whether a basic MSC is contained in another MSC diagram.
Client Interface Server
~~~h i~—i i—i
	—JJfSister		
		Register	
	Response	-*	
	4-- Request		
		-"-► Response	
	<---		
			
Specification
15/17
Find Flow function checks whether a basic MSC is contained in another MSC diagram.
Client Interface Server Client Interface Server
~~~h i——I r—□ i——| r——I i——I
	—JJfSister					
		Register ~->		Respond-		
	<-~ Request			Request	■—Register	
		Response			--► Response	
				4--"		
Specification Flow
15/17
Find Flow function checks whether a basic MSC is contained in another MSC diagram.
Client Interface Server Client Interface Server
~~~h r——I r—□ i——i r——I i——i
						
	Response 4-—■-	Register		Respond-.	■—*£9jster	
		->				
	Request			Request		
		Response			--► Response	
				4--"		
Specification Find Flow result
15/17
Summary
• drawing aids
• easy and comfortable drawing
• message flipping, shortcuts, .. .
• transformers Beautify, Tighten Time, .
• verification & validation tools
o (Time) Race checker
» Time Consistency checker
• Strong Readability checker
• additional functions
• Find Flow
• Monte Carlo simulation (experimental)
16/17
Summary
drawing aids
easy and comfortable drawing message flipping, shortcuts, .. . transformers Beautify, Tighten Time, .
verification & validation tools
(Time) Race checker Time Consistency checker Strong Readability checker
additional functions
Find Flow
Monte Carlo simulation (experimental)
16/17
Summary
drawing aids
easy and comfortable drawing message flipping, shortcuts, .. . transformers Beautify, Tighten Time, . .
verification & validation tools
(Time) Race checker Time Consistency checker Strong Readability checker
additional functions
Find Flow
Monte Carlo simulation (experimental)
SCStudio is available on sourceforge.net
16/17
Thank you for your attention
INVESTICE DO ROZVOJE VZDĚLÁVÁNI
17/17