PA160: Net-Centric Computing II. Specification and Verification of Network Protocols Vojtěch Řehák Faculty of Informatics, Masaryk University Spring 2014 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 1/95 Theory Definition and Usage Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 2 / 95 Theory Definition and Usage Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 2 / 95 Theory Definition and Usage Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 2 / 95 Theory Definition and Usage Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 2 / 95 Theory Definition and Usage Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 2 / 95 Theory Definition and Usage Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 2 / 95 Theoretical Results as Tools for Users Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 3 / Formal Models - what are they good for The basic concept is a model of system (i.e. the object we work with). thought handling • individual approach (intra-brain) - to grasp it • documentation (inter-brain) - to pass it on automatic/computer processing (comparing model to specification) • testing • simulation • symbolic execution • static analysis • model checking • equivalence checking • theorem proving Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 4 / 95 Formal Models in Specification natural language vs. formal language freedom in writing human resources restrictions in writing automatic methods Formal Models in Specification natural language vs. formal language freedom in writing restrictions in writing human resources automatic methods nothing < text < structured text < text with formal "pictures" < formal description with informal comments < complete formal description Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 5 / 95 Formal Models in Specification natural language vs. formal language freedom in writing restrictions in writing human resources automatic methods nothing < text < structured text < text with formal "pictures" < formal description with informal comments < complete formal description Goal: Find an appropriate level of abstraction and keep it. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 5 / 95 Formal Models in Specification natural language vs. formal language freedom in writing restrictions in writing human resources automatic methods nothing < text < structured text < text with formal "pictures" < formal description with informal comments < complete formal description Goal: Find an appropriate level of abstraction and keep it. "What will be the model used for?" Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 5 / 95 Map - Abstraction Example Map - Abstraction Example Map - Abstraction Example "Model has to suit its purpose!" Only relevant information are presented; no more, no less. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 6 / 95 Outline Models we will talk about: • Message Sequence Charts (MSC) • Specification and Description Language (SDL) • Petri nets • Queueing theory What they can be used for? • modelling • specification • analysis • simulation • testing • partial implementation Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 7 / 95 Distributed Systems "What is the problem of distributed systems?" Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 8/95 Distributed Systems - Key characteristics (Déja vu) Key Characteristics of Distributed Systems: • Autonomicity - there are several autonomous computational entities, each of which has its own local memory • Heterogeneity - the entities may differ in many ways • computer HW (different data types' representation), network interconnection, operating systems (different APIs), programming languages (different data structures), implementations by different developers, etc. • Concurrency - concurrent (distributed) program execution and resource access • No global clock - programs (distributed components) coordinate their actions by exchanging messages • message communication can be affected by delays, can suffer from variety of failures, and is vulnerable to security attacks • Independent failures - each component of the system can fail independently, leaving the others still running (and possibly not informed about the failure) • How to know/differ the states when a network has failed or became unusually slow? • How to know if a remote server crashed immediately? Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 9 / 95 Distributed Systems Vojtěch Řehák (Fl MU) Specification and Verification Distributed Systems Distributed vs. Local SDL Specification Description Language MSC Message Sequence Chart ITU-T Z.100 ITU-T Z.120 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 11 / 95 Distributed vs. Local SDL Specification Description Language ITU-T Z.100 models of components MSC Message Sequence Chart ITU-T Z.120 communication model Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 11 / 95 Message Sequence Chart (MSC) Message Sequence Chart (MSC) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 12 / 95 Message Sequence Chart (MSC) international standard of ITU-T, Z.120 • 1993 - first version of Z.120 recommendation 9 . .. • 2011 - current version of Z.120 recommendation • all documents of the current version: • Z.120 - Message Sequence Chart (MSC) » Z.120 Annex B - Formal semantics of message sequence charts • Z.121 - Specification and Description Language (SDL) data binding to Message Sequence Charts (MSC) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 13 / 95 Message Sequence Chart (MSC) international standard of ITU-T, Z.120 • 1993 - first version of Z.120 recommendation 9 . .. • 2011 - current version of Z.120 recommendation • all documents of the current version: • Z.120 - Message Sequence Chart (MSC) » Z.120 Annex B - Formal semantics of message sequence charts • Z.121 - Specification and Description Language (SDL) data binding to Message Sequence Charts (MSC) It formally defines both textual and graphical form. MSC is a similar concept to UML Sequence Charts. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 13 / 95 Message Sequence Chart (MSC) A trace language for the specification and description of the communication behaviour by means of message exchange. Describes • communicating processes, • communication traces, • message order, • time information (timeouts, constraints), • high-level form for set of traces. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 14 / 95 Message Sequence Chart (MSC) msc diagram msc heading condition output event input event msc User_accepted User AC System Idle a Code OK Card out > Unlock Door unlocked instance message to the environment instance end Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 15 / 95 Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 16 / 95 Message Sequence Chart (MSC) - semantics Peter Jane Paul Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 16/95 Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 16/95 MSC - Visual Order Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 17/95 MSC - Visual Order - Hasse Diagram MSC Properties What is an unwanted behaviour/property? Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 19 / 95 MSC Properties What is an unwanted behaviour/property? Fundamental problems in the specified model, e.g. an implementation of the model does not exist in the given environment. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 Acyclic/Cyclic property cyclic dependency among events Instance p Instance q unrealizable in any environment Spring 2014 20 / 95 Acyclic/Cyclic property FIFO/non-FIFO property overleaping messages Instance p Instance q Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 22 / 95 FIFO/non-FIFO property overleaping messages Instance p Instance q unrealizable in an environment preserving message order Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 22 / 95 FIFO/non-FIFO property overleaping messages Instance p Instance q Instance p Instance q Instance r □ unrealizable in an environment preserving message order Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 22 / 95 FIFO/non-FIFO property overleaping messages Instance p Instance q Instance p Instance q Instance r □ unrealizable in an environment preserving message order realizable in an environment with P2P channels but unrealizable in case of one global channel Vojtěch Řehák (Fl MU) Spring 2014 22 / 95 Jane Paul Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 23 / 95 Race Condition Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 23 / 95 Race Condition Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 23 / 95 Solution #1 - Coregion Construction Let us demonstrate that some events are not ordered. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 24 / 95 Solution #1 - Coregion Construction Let us demonstrate that some events are not ordered. Peter Jane Paul Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 24 / 95 Solution #1 - Coregion Construction Let us demonstrate that some events are not ordered. Peter Jane Paul Events in a coregion are not order; except for the event related by general ordering. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 24 / 95 Solution #2 - List/set of all possibilities Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 25 / 95 High-Level MSC (HMSC) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 26 / 95 High-Level MSC (HMSC) - ITU-T Z.120 msc ACsystemOverview _-connection point -HMSC start User rejected msc reference -restrictive condition alternative Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 27 / 95 High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák (Fl MU) Specification and Verification High-Level MSC (HMSC) - ITU-T Z.120 HI Trace example: Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 28 / 95 High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 28 / 95 High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 28 / 95 High-Level MSC (HMSC) - ITU-T Z.120 H-I £H HI Trace example: these events are not ordered! Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 28 / 95 High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 28 / 95 High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 28 / 95 High-Level MSC (HMSC) - ITU-T Z.120 28 / 95 High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 28 / 95 High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 28 / 95 Deadlock Property 29 / 95 ivelock Property Vojtěch Řehák (Fl MU) Membership Is a given MSC included in a given HMSC? Vojtěch Řehák (Fl MU) Specification and Verificatio Membership Is a given MSC included in a given HMSC? Instance A Instance B III P „ ^ q 4 q 4 q 4 q ^ q q Input BMSC bMSCOl bMSC02 Input HMSC Instance A Instance B 1 r Instance A Instance B I I L q Vojtěch Řehák (Fl MU) Specification and Verificatioi Spring 2014 31 / 95 Inline Expressions Systeml System2 System3 ' , i i , "i i altj ] Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 32 / 95 Inline Expressions Systeml System2 System3 ' , i i , "i i altj ] Other inline expression types: opt, loop(m,n), exc, seq, par. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 32 / 95 Non-local Choice System 1 System2 System3 altj --—— I 1 I ~1 I ~l Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 33 / 95 Non-local Choice System 1 System2 System3 altj --—— I 1 I ~1 I ~l System3 does not know which alternative has been chosen. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 33 / 95 Non-local Choice Systeml System2 System3 altj "---~^top ■——£S2£Í2ue__^ ' ' ' ' ' ' Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 33 / 95 Non-local Choice Systeml System2 System3 altj "---~^top ■——£S2£Í2ue__^ ' ' ' ' ' ' ' ' ' System3 does not know which alternative has been chosen. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 33 / 95 Universal Boundedness What is the size of input buffer of Y that will never overflow? M Universal Boundedness What is the size of input buffer of Y that will never overflow? Every finite input buffer of Y can overflow. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 34 / 95 Universal Boundedness What is the size of input buffer of Y that will never overflow? 34 / 95 Universal Boundedness What is the size of input buffer of Y that will never overflow? Buffers of size 1 will never overflow. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 34 / 95 Existential Boundedness The system deadlocks in case of FIFO channels (and FIFO buffers). What is the size of non-FIFO buffer needed to avoid deadlock (in case of FIFO channels)? Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 35 / 95 Existential Boundedness The system deadlocks in case of FIFO channels (and FIFO buffers). What is the size of non-FIFO buffer needed to avoid deadlock (in case of FIFO channels)? Buffer of size 2 suffices to avoid deadlock. Or one buffer for each message label (type). Spring 2014 35 / 95 Race Condition - Solution #3 - Time Constraints Application server Spring 2014 36 / 95 Race Condition - Solution #3 - Time Constraints Client Proxy Application server 36 / 95 Race Condition - Solution #3 - Time Constraints Client Proxy Application server --__^fSf/ster s ---Register t m Response^___—— 1 Message Response -4----- "A Vojtěch Řehák (Fl MU) Specification ai ind Verification ing 2014 36 / 95 Time Consistency Are the given time conditions consistent? Client A Proxy Server A" HTTP, Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 37 / 95 Time Tightening Some time conditions can be tightened. Client A Proxy Server 38 / 95 Time Tightening Some time conditions can be tightened. Client A Proxy Server 38 / 95 Timers ICONreq Initiator Responder ICON alt LATECONF ICONF iX- OKCONF ICONF Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 39 / 95 MSC - Summary Basic MSC • instances • messages • send events • receive events • conditions • coregions • general ordering • inline expressions • time constraints • timers High-level MSC (HMSC) • start node • end node • reference nodes • connection points • lines • conditions • time constraints Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 40 / 95 MSC - Properties • Acyclic property • FIFO property • Race Condition • Deadlock • Livelock • Membership • Nonlocal Choice • Universal Boundedness • Existential Boundedness • Time Race Condition • Time Consistency • Tighten Time Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 41 / 95 MSC - Goals What MSC is good for? Both human and computer readable formalizm • basic behaviour demonstration (use cases), • high level system behaviour description, • test case specification, and • (test) log visualization. Vojtěch Řehák (Fl MU) Specification and Verification MSC - Goals What MSC is good for? Both human and computer readable formalizm for: • basic behaviour demonstration (use cases), • high level system behaviour description, • test case specification, and • (test) log visualization. What MSC is NOT good for? detailed specification (before implementation), hierarchical structure of communicating entities, implementation details (primitives for communication, detailed data manipulation), etc. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 42 / 95 MSC - Tools Mesa • academic tool • local choice and time checkers MSCan • academic tool • only textual input • some checkers IBM Rational, SanDriLa SDL, Cinderella SDL Sequence Chart Studio (SCStudio) • MS Visio addon • drawing, import, export • checkers for all the mentioned properties Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 43 / 95 Sequence Chart Studio MSC drawing and verification tool developed at Fl MU. http://scstudio.sourceforge.net Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 44 / 95 Distributed vs. Local SDL Specification Description Language ITU-T Z.100 models of components MSC Message Sequence Chart ITU-T Z.120 communication model Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 45 / 95 Specification Description Language (SDL) Specification Description Language (SDL) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 46 / 95 Specification Description Language (SDL) international standard of ITU-T, Z.100 • 1972 - Establishment of a working group for SDL • 1976 - first version of Z.100 recommendation «... • 12/2011 - current version of Z.100 recommendation • all documents of the current version: • Z.100 - Specification and Description Language (SDL) • Z.100 Supplement 1 - SDL+ methodology: Use of MSC and SDL • Z.lmplOO - SDL implementer's guide a Z.101 - SDL - Basic SDL-2010 a Z.102 - SDL - Comprehensive SDL-2010 0 Z.103 - SDL - Shorthand notation and annotation in SDL-2010 0 Z.104- SDL - Data and action language in SDL-2010 0 Z.105 - SDL - SDL-2010 combined with ASN.l modules a Z.106 - SDL - Common interchange format for SDL a Z.108 - SDL - Object-oriented data in SDL-2010 a Z.109 - SDL - UML profile for SDL-2010 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 47 / 95 SDL - Specification Description Language An object oriented languages for specification of applications that are • heterogeneous, • distributed (concurrent), • interactive (event-driven, discrete signals), and • real-time dependent (with delays, timeouts). Describes • structure (distributed components of the system), • behaviour (instructions within the components), and • data of distributed systems in real-time environments. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 48 / 95 SDL - representations Three representations: SDL/GR graphical representation (human readable) SDL/PR textual phrase representation (machine readable) SDL/CIF common interchange format (SDL/PR with graphical information) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 49 / 95 SDL - representations Three representations: SDL/GR graphical representation (human readable) SDL/PR textual phrase representation (machine readable) SDL/CIF common interchange format (SDL/PR with graphical information) In what follows, we focus on the graphical representation (SDL-GR). Basic SDL components • system and blocks (structure) • processes and procedures (behaviour) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 49 / 95 SDL/GR - Process process type diagram. process type Controller 1(1] del cjr_panel Pld ^current panel whose Code will be validated 7 " ~~ del cid, PIN integer ;/* temporary variables for the data attributes of Code' 7 3- LfipUl \Code(old,PIN^, XT Iran Fanal'/ _task cur_panel -SENDER OK P from Central */ TO unlOCkDoor Central Unit 7 ^ Va'dation ^ ( idle ) ^ unlOCkDoor ^ procedure I'L'l L' IV I IL L' NOK r Irom Central */ OK \ TO curpanel/ NOK TO cur_pane procedure call \ output Vojtěch Řehák (Fl MU) Specification and Verification mir Tpxthnnk \/4 0 Spring 2014 50 / 95 SDL/GR - Procedure procedure GetPIN fpar In/out pin Integer, IN no_dig Integer del d Integer; t digit value 7 del i Integer; !* rjnner 0:no_dig */ pin := 0 . i :=0 Wait Digit 1 Digit (d) pin := pin*10 + d ( WaitDigit \ from Keyboard procedure "start Vojtěch Řehák (Fl MU) Specification and Verification source: TIMe Electronic Textbook v4.0 Spring 2014 51 / 95 SDL/GR - Block block (type) heading text ' symbol signal opened.dosed ; /* Door -s Controller */ <— slgnal open, close ; /* Controller -> Door 7 :» /"signal lists (inp), (out) and (validity)defined in enclosing block. This Holds also for signal 'Code' */ KinpH [(OLltp)] j block type AceessPoiffi 1(1) Controller ■ [(inp)]. Koutpn 1 Panel pi p ape: Controller [(validity)] [code] [opened, closed] [(validity)] CU [Code] signal definitions [isOpen, isClosed] [(validity)] [Code] gate signal list blocktype diagram \ signalronte Vojtěch Řehák (Fl MU) Specification and Verification source: TIMe Electronic Textbook v4.0 Spring 2014 52 / 95 SDL/GR - Block with block structure block type diagra text y symbol e [(Imp)] [(outp)] block (type) heading block type AccessPoint 1(1! signal opened .closed ; /* Door TO Controller 7 signal open, close ; /* Controller TO Door */ CEJnp)] i gate signal list Panel Door [(validity); P1 [code; Controller cu [open, close] [(validity).] [Code] signal definitions C [Code] [(validity]] block (single) '■■.channel Vojtěch Řehák (Fl MU) Specification and Verification source: TIMe Electronic Textbook v4.0 Spring 2014 53 / 95 SDL/GR - System (the top most block) system AccessContro 1(1) /* Signal definitions for AccessPoint communication 7 SIGNAL eject-card, lock, unlock /■ AccessPoint input-card, isopen, isClosed r ENV display, /■ Display keys; /• ENV SIGNAL Code(integer,inteaer);/' AccessPoint SIGNAL OK.NOK.ERR ; /• CentralUnit TO ENV 7 TO Access Points TO ENV "1 TO Keyboard */ TO CentralUnit */ TO AccessPoint V SIGNALLIST validity = OK, NOK, ERB ; SIGNALLIST outp . EjectGard, display; SIGNALLIST inp = InpjtCard, keys ; block lype (reference) list Vojtěch Řehák (Fl MU) signal block set accord i rig to a block type Specification and Verification block (single) source: TIMe Electronic Textbook v4.0 Spring 2014 54 / 95 SDL/GR - Channels Nondelaying channels for "immediate" message delivery (e.g., between processes within a computer). ■ < Delaying channels for "time consuming" message delivery Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 55 / 95 Summary of SDL Basics System - is the top most block surrounded by environment. Block - consists of blocks or processes that are connected by channels. - expresses the hierarchical structure of the system. - its names are references to other objects. Process - sends and receives messages. - stays in states. - can call procedures. Procedure - is a subroutine that can finish. - does not return any value (only in variables or sent messages). Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 56 / 95 Message Exchange - Operational Semantics • one input buffer for a process • FIFO behaviour • no priority queues • signal which is unspecified in the current state is discarded Vojtěch Řehák (Fl MU) Specification and Verification source: TIMe Electronic Textbook v4.0 Spring 2014 57 / 95 Asterisk Save, Asterisk State, and Dash State process type heading redefined process type «block type BlockingAccessPoint>> Controller Inherits <] Access Point 6 AP(100): C Access Point d CD [(validity)] [Code] CentralUnit i ([IsO pen, is Closed] i1 [lock,unlock] source: TIMe Electronic Textbook v4.0 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 60 / 95 Multiple Instances of a Process Hewgame Game /--\ Block Blockgame SIGNAL Gameover (Piď), I Gameoverack; Jßumpj Monitor (1,1) Bump, Gameoveiack i3ame(0,) Gameid, Win, L.o st, 3 :i:ire D e am on s e rver. out Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 Additional SDL Constructs • Asterisk save, asterisk state, and dash state • Timer construction • Multiple block instances (no dynamic creation) • Multiple process instances (with dynamic creation and limit) • Packages collections of related types and definitions (library) • Subtypes • Virtual processes 0 Process type redefinition and finalization • Inherited blocks Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 62 / 95 SDL - Overview tíäígrxatt heading system example sysle m example system example c3 d1 031 -5 |>>] cl 3i3j block b1 2(3) block b1 1(31 b1,1 1 rl [{=1)] [W] ^T1 Systems and blocks am contain ^ blocks tmaYorpmcesses. "** process p2 2(211 1(211 process p2 ^_ initial a P/rx'esses contain / behaviour ana1 cannot ŕ contain blocks. procedjre pr 111 ■ Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 63 / 95 SDL - Goals What SDL is good for? SDL is designed for unambiguous specification of requirements and description of implementation of the normative requirements of telecommunication protocol standards. For computer based tools to improve the process of • specification (create, maintain, and analyze), and • implementation (automatic code generation). Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 64 / 95 SDL - Goals What SDL is good for? SDL is designed for unambiguous specification of requirements and description of implementation of the normative requirements of telecommunication protocol standards. For computer based tools to improve the process of • specification (create, maintain, and analyze), and • implementation (automatic code generation). What SDL is NOT good for? high level system description (what the system serves for), demonstration of good or wrong behaviour, test trace specification, implementation details (primitives for communication, detailed data manipulation), etc. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 64 / 95 MSC and SDL in Workflow • typical/optimal communication sequences (MSC) • error sequences (MSC) • optionally - full specification in (HMSC) • distributed specification (SDL) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 65 / 95 MSC and SDL in Workflow • typical/optimal communication sequences (MSC) • error sequences (MSC) • optionally - full specification in (HMSC) • distributed specification (SDL) Formal model benefits • (H)MSC to SDL transformation (realization) • SDL to source code transformation (implementation) • MSC to test case transformation • simulation to MSC transformation (membership checking) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 65 / 95 SDL - Tools IBM Rational • from tools of Telelogic (SDT, Geode, Tau a drawing, import, export • automatic implementation in C++ • simulation support SanDriLa SDL • MS Visio stencil • drawing, import, export • analyses of states in process diagrams • open for addons Cinderella SDL • modelling, import, export • analyses and simulation Vojtěch Řehák (Fl MU) Specification and Verification Petri Nets Petri Nets Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 67 / 95 Petri Nets C. A. Petri: Kommunikation mit a Basic components: • places • transitions • tokens • arcs Marking = configuration = distribution of tokens = vector of #s of tokens in places maten, 1962 places with tokens inside A transition can be fired if there is a token in each of its input places. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 68 / 95 Petri Nets C. A. Petri: Kommunikation mit automaten, 1962 Basic components: • places • transitions • tokens • arcs Marking = configuration = distribution of tokens = vector of #s of tokens in places input places output places Tokens from input places are removed and new tokens are added into the output places of the fired transition. Demonstration Example #1 69 / 95 Demonstration Example #1 Demonstration Example #2 Better and a bit more complicated example. 70/95 Basic Constructions Sequential execution Alternative Parallel execution Iteration f\ 3 / \ Ď I 3 i ° 1 V T T Tl O O O Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 71 / 95 Basic Constructions Semaphore Rende-vous 72 / 95 Basic Constructions Basic Constructions Basic Constructions T T T T b a TYyT t< Critical section Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 73 / 95 Basic Constructions T T T T b a TYyT t< Critical section Vojtěch Řehák (Fl MU) Alternation Specification and Verification Spring 2014 73 / 95 Basic Constructions T T T T T T Basic Constructions T T T T T T Different Modifications/Extensions of Petri Nets • Condition-Event Petri nets (C-E PN) • Place-Transition Petri nets (P-T PN) a Coloured Petri nets • Hierarchical Petri nets • Timed Petri nets • Time Petri nets • Stochastic Petri nets Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 74 / 95 Condition-Event Petri Nets In this case: • places = conditions • transitions = event An event/transition is enabled if and only if • all its pre-conditions are true and • all its post-conditions are false. I.e., an event occurrence negates its pre- and post-conditions. Therefore, there is one or none token in each place. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 75 / 95 Transition-Place Petri Nets An arbitrary number of tokens in each place, producer transp. channel o—I—o ( • )"— consumer Ó notification channel Producer-consumer model for bounded transport channel. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 76 / 95 Additional Constructs - Arc Multiplicity 77 / 95 Additional Constructs - Inhibitor and Reset Arcs O An inhibitor arc imposes the precondition that the transition may only fire when the place is empty. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 78 / 95 Additional Constructs - Inhibitor and Reset Arcs O o An inhibitor arc imposes the precondition that the transition may only fire when the place is empty. A reset arc does not impose a precondition on firing, and empties the place when the transition fires. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 78 / 95 Properties of Petri nets • reachability - reachability tree or coverability tree • bounded (safe) places • a place with a bound on the number of its tokens in all reachable markings • a place is safe if the number of its tokens < 1 in all reachable markings • liveness • a transition is live if, from every marking, one can reach a marking where the transition is enabled • a net is live if all its transitions are live 79 / 95 Properties of Petri nets • p-invariant • an invariant vector on places, i.e. a multiset of places representing weighting such that any such weighted marking remains invariant by any firing, e.g. 3 * pi + P2 + P3 + P4 + P5 + 3 * p6. • t-invariant • an invariant vector on transitions, i.e. a multiset of transitions whose firing leave invariant any marking, e.g. ti + 2 * £2 + £3 + £4 + £5. p2 12 p3 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 80 / 95 Coloured Petri Nets Different colours (classes) of tokens. 3'p+2'q+5'r 3'p+l'q+2'r o o marking expression, arc expression, transition guard (next slide) Colours usually serves for data type representation. Vojtěch Řehák (Fl MU) Spring 2014 81 / 95 Coloured Petri Net Example Hierarchical Petri Nets source: http://www.gridworkflow.org/kwtgrid/gwes-web/ Time PN, Timed PN, Stochastic PN, priority nets • priorities of concurrent transitions time (or timed-arc) nets • tokens has its lifetime, arcs to transitions are labeled by time intervals of required ages of tokens timed nets • firing starts when a transition is enabled but it takes some specified time to produce output stochastic nets • probability distribution on time to fire (exponential, deterministic, or general distributions) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 84 / 95 PN Tools CPN Tools • Coloured Petri Nets (with prioritized transitions and real time support) • editor, simulation, analyses Tapall • Timed-Arc Petri Nets (with real time support) • editor, simulation, compositional models, TCTL logic checker TimeNET • Coloured and Stochastic PN with non-exponential distributions • editor, simulation, analyses (p-invariant, performance analyses) SNOOPY, TINA - Time petri Net Analyzer, Romeo, . .. And many more tools and use cases, see, e.g. http://www. informatik. uni-hamburg.de/TGI/Petri Nets/tools/quick, htm I http://cs.au.dk/cpnets/industrial-use/ Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 85 / 95 Queueing theory Queueing theory Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 86 / 95 Queueing theory In 1909 A.K. Erlang, a danish telephone engineer, was asked: "What the queue capacity should be of the central telephone switch in Copenhagen?" Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 87 / 95 Queueing theory In 1909 A.K. Erlang, a danish telephone engineer, was asked: "What the queue capacity should be of the central telephone switch in Copenhagen?" Our motivation example: 30 customers will visit the Machine in an hour. Each will use it for a minute and a half. How busy is the Cash Machine? For how long time does a customer wait (on average)? Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 87 / 95 Questioning about Queues Generator Queue of customers © mean number of queueing (and being served) req © mean service and queueing time © mean system delay (empty queue) © how many servers do I need to . .. Vojtěch Řehák (Fl MU) Specification and Verification Queue parameters - Kendall Notation A/S/n/B/K/SD A - interarrival-time distribution G - general, M - Poisson, D - deterministic.. . S - service time distribution G - general, M - exponential, D - deterministic.. . n - number of servers 1, 2.....oo B - buffer size (the max. number of waiting and served requests) 1, 2.....oo K - population size 1, 2.....oo SD - service discipline FIFO, LIFO, Random, RR - Round Robin E.g., M/G/l/oo Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 89 / 95 Queueing Networks Apache - MaxClients = 100 Web Server 1 J" 3 • open and closed networks • system dependences • traffic intensity • occupancy (on different servers), bottleneck detection, • very similar to Stochastic Petri Nets Reply Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 90 / 95 Solutions / Question answering General solution: • simulation For specific types of queues: • analytical results Solutions / Question answering General solution: • simulation For specific types of queues: • analytical results Our motivation example: 30 customers will visit the Machine in an hour. Each will use it for a minute and a half. How busy is the Cash Machine? What is the average waiting time? Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 91 / 95 Solutions / Question answering General solution: • simulation For specific types of queues: • analytical results Our motivation example: 30 customers will visit the Machine in an hour. Each will use it for a minute and a half. How busy is the Cash Machine? What is the average waiting time? Solution if the queue is M/M/l/oo: The utilization of the Cash Machine is 45 minutes in an hour, i.e. 75%. Average number of customers at the Cash Machine is 75/(100 — 75) = 3. I.e., the average waiting of a customer is 4.5 minutes. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 91 / 95 Little's Law Theorem The long-term average number of customers in a stable system L is equal to the long-term average effective arrival rate, A, multiplied by the average time a customer spends in the system, W. I.e. _L = A • W._ Although it looks intuitively reasonable, it is quite a remarkable result, as the relationship is "not influenced by the arrival process distribution, the service distribution, the service order, or practically anything else." Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 92 / 95 Tools for Queueing Systems G/M/c-like queue • online steady-state solution of a G/M/c-like queue • http://queueing-systems.ens-lyon.fr/formGMC.php Queueing Simulation • online queueing network analyzer • http://www.stat.auckland.ac.nz/~stats255/qsim/qsim.html JMT - Java Modelling Tools • framework for model simulation and workload analysis • http://jmt.sourceforge.net/ SimEvents • simulation engine and component library for Simulink (MATLAB) • http://www.mathworks.com/products/simevents/ Up-to-date List of relevant Queueing theory based tools: http://web2.uwindsor.ca/math/hlynka/qsoft.html Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 93 / 95 Relevant Lectures IV113 Úvod do validace a verifikace (Barnat) IV109 Modelování a simulace (Pelánek) IA159 Formal verification methods (Strejček) PV177 Laboratoř pokročilých síťových technologií (Řehák) IA158 Real Time Systems (Brázdil) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 94 / 95 References • ITU-T recommendation Z.120: Message Sequence Charts (MSC). 2011. • ITU-T recommendation Z.100: Specification Description Language (SDL). 2011. • S. Mullender. Distributed Systems. ACM, 1993. • D. Peled. Software Reliability Methods. Springer, 2001. 9 R. Braek at al. TIMe: The Integrated Method. SINTEF, 1999. • L. Doldi. Validation of Communications Systems with SDL. Wiley, 2003. • M. Broy and K. St0len. Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, 2001. • W. Jia and W. Zhou. Distributed Network Systems: From Concepts to Implementation. Springer, 2005. • M. Češka. Petriho sítě. Akademické nakladatelství CERM Brno, 1994. • J. Markl. Petriho sítě. VŠB - Technická univerzita Ostrava, 1996. • G. Giambene. Queuing Theory and Communications - Networks and Applications. Springer, 2005. • D. Gross at al. Fundamentals of Queuing Theory. Wiley, 2008. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2014 95 / 95