PA160: Net-Centric Computing II. Specification and Verification of Network Protocols Vojtgch Rehak Faculty of Informatics, Masaryk University Spring 2016 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 1/97 Theory Definition and Usage Theory Definition and Usage Theory Definition and Usage Theory Definition and Usage Theory Definition and Usage Theoretical Results as Tools for Users J Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 /97 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 9 equivalence checking • theorem proving Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 Formal Models in Specification natural language vs. formal language freedom in writing O human resources © O restrictions in writing © automatic methods Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 5/97 Formal Models in Specification natural language vs. formal language freedom in writing O © restrictions in writing human resources © O 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 2016 5 / 97 Formal Models in Specification natural language vs. formal language freedom in writing Q © restrictions in writing human resources © O 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 2016 5 / 97 Formal Models in Specification natural language vs. formal language freedom in writing Q © restrictions in writing human resources © O 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 2016 5/97 Map - Abstraction Example Find Pardubice or directions from Brno to Liberec, source: www.mapy.cz Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 6/97 Map - Abstraction Example Find Pardubice or directions from Brno to Liberec. source: www.mapy.cz Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 6 / 97 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 2016 6 / 97 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 9 specification • analysis • simulation • testing • partial implementation Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 7 / 97 Distributed Systems "What is the problem of distributed systems?" J Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 8/97 Distributed Systems - Key characteristics (Dejä vu) Key Characteristics of Distributed Systems: o Autonomicity - there are several autonomous computational entities, each of which has its own local memory o 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) o How to know/differ the states when a network has failed or became unusually slow? ^^^^^^^Howtoknowi^a remoteserver crashed immediatelv^^^^^^^^^^^^^^^^^ Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 9 / 97 Distributed Systems Distributed Systems Human way of thinking is sequential Specification and Verification Spring 2016 10 / 97 World is distributed Vojtěch Řehák (Fl MU) 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 2016 Distributed vs. Local SDL Specification Description Language MSC Message Sequence Chart ITU-T Z.100 íttpUÍ 1 > (Telephone ^ oi>hoolc J 1 Caller goes off-hook Caller gels ikll KJIU- T <1^^> ^ Dial lone J) J— J 1 Language symbols Graphical specification ITU-T Z.120 CmtltiaC'l l'r'-,r]|| t|i,| H*ic|iLnil hrM IlLChl Iii rl 11' II i- AittH'.iflllHltllMH HUTS U.U.UlUllfarlu i models of components communication model Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 Message Sequence Chart (MSC) Message Sequence Chart (MSC) J Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 12 / 97 Message Sequence Chart (MSC) international standard of ITU-T, Z.120 • 1993 - first version of Z.120 recommendation • ... • 2011 - current version of Z.120 recommendation 9 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 2016 13 / 97 Message Sequence Chart (MSC) international standard of ITU-T, Z.120 • 1993 - first version of Z.120 recommendation • ... • 2011 - current version of Z.120 recommendation 9 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 2016 13 / 97 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 2016 14 / 97 Message Sequence Chart (MSC) msc diagram msc heading condition output event input event msc User_accepted User AC System Idle Code OK Card out Unlock Door unlocked instance message to the environment instance end Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 15 / 97 Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 16 / 97 Message Sequence Chart (MSC) - semantics Peter Jane Paul Message Sequence Chart (MSC) - semantics Peter Jane Paul Message Sequence Chart (MSC) - semantics Peter Jane Paul MSC - Visual Order Peter Jane Paul Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 17 / MSC - Visual Order - Hasse Diagram Peter Jane Paul Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 18 / 97 MSC Properties What is an unwanted behaviour/property? Vojtěch Řehák (Fl MU) Specification and Verification 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 2016 19 / 97 Acyclic/Cyclic property cyclic dependency among events Instance p Instance q unrealizable in any environment J Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 20 / 97 Acyclic/Cyclic property Client Manager Software Architect Make a product Prototype Make a product Q Prototype Spring 2016 21 / 97 FIFO/non-FIFO property overleaping messages Instance p Instance q Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 22 / 97 FIFO/non-FIFO property overleaping messages Instance p Instance q unrealizable in an environment preserving message order J Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 22 / 97 FIFO/non-FIFO property overleaping messages Instance p Instance q Instance p Instance q Instance r m2 --► m3 unrealizable in an environment preserving message order Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 22 / 97 FIFO/non-FIFO property overleaping messages Instance p Instance q Instance p Instance q Instance r unrealizable in an environment preserving message order J realizable in an environment with P2P channels but unrealizable in case of one global channel Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 22 / 97 Race Condition Peter Jane Paul Race Condition Peter Jane Paul Race Condition Peter Jane Paul Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 23 / 97 Solution #1 - Coregion Construction Let us demonstrate that some events are not ordered. Specification and Verification Solution #1 - Coregion Construction Let us demonstrate that some events are not ordered. Peter Jane Paul Solution #1 - Coregion Construction Let us demonstrate that some events are not ordered Peter Jane Paul Ma Yes- 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 2016 24 / 97 Solution #2 - List/set of all possibilities Vojtěch Řehák (Fl MU) Specification and Verification High-Level MSC (HMSC) High-Level MSC (HMSC) - ITU-T Z.120 High-Level MSC (HMSC) - ITU-T Z.120 High-Level MSC (HMSC) - ITU-T Z.120 Specification and Verification Spring 2016 28 / 97 High-Level MSC (HMSC) - ITU-T Z.120 High-Level MSC (HMSC) - ITU-T Z.120 High-Level MSC (HMSC) - ITU-T Z.120 Trace example: these events are not ordered! Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 28 / 97 High-Level MSC (HMSC) - ITU-T Z.120 High-Level MSC (HMSC) - ITU-T Z.120 High-Level MSC (HMSC) - ITU-T Z.120 High-Level MSC (HMSC) - ITU-T Z.120 High-Level MSC (HMSC) - ITU-T Z.120 Deadlock Property Specification and Verification Livelock Property "A i B Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 30 / 97 Membership Is a given MSC included in a given HMSC? Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 31 / 97 Membership Is a given MSC included in a given HMSC? Instance A Instance B P Input BMSC Vojtěch Řehák (Fl MU) bMSCOI í "A bMSC02 Input HMSC Instance A Instance B bMSCOI Instance A Instance B 1 q bMSC02 Specification and Verification Spring 2016 Inline Expressions System 1 System2 System3 i , i i "i i "i alt] Stop I —I I —I I —I Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 32 / 97 Inline Expressions System 1 System2 System3 i , i i "i i "i alt] Stop I I I I I I Other inline expression types: opt, loop(m, n), exc, seq, par. Vojtěch Řehák (Fl MU) Specification and Verification Spring Non-local Choice System 1 System2 Sy stem3 i —i i —i i —i altj ■ I ■ I I ■ Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 Non-local Choice System 1 System2 i —i i —i System3 i —i altj System3 does not know which alternative has been chosen j Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 33 / 97 Non-local Choice System 1 System2 System3 alt] '-----Jl^rupt Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 33 / 97 Non-local Choice System 1 System2 Systems i ~i Interru pt System3 does not know which alternative has been chosen j Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 33 / 97 Universal Boundedness What is the size of input buffer of Y that will never overflow? x M Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 34 / 97 Universal Boundedness What is the size of input buffer of Y that will never overflow? x M Every finite input buffer of Y can overflow. j Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 34 / 97 Universal Boundedness What is the size of input buffer of Y that will never overflow? Y M M Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 34 / 97 Universal Boundedness What is the size of input buffer of Y that will never overflow? Y M M Buffers of size 1 will never overflow. j Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 34 / 97 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)? Spring 2016 35 / 97 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)? Instance p Instance q Buffer of size 2 suffices to avoid deadlock. Or one buffer for each message label (type) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 35 / 97 Race Condition - Solution =^=3 - Time Constraints Client Proxy Application server Specification and Verification Spring 2016 Race Condition - Solution =^=3 - Time Constraints Application server Resp onse Message agister Response Response Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 Race Condition - Solution =^=3 - Time Constraints Client Proxy Application server Message Re^ponse____ ^^^^1 ^^^^H ^^^^1 Specification and Verification Spring 2016 Time Consistency Are the given time conditions consistent? Client A A" o r, O I Ý. Proxy Server HTTP Resp onse HTTP response o in Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 37 / 97 Time Tightening Some time conditions can be tightened Client A Proxy A" o r, O I Y". HTTP Resp onse HTTP response Vojtěch Řehák (Fl MU) Specification and Verification Time Tightening Some time conditions can be tightened Client A Proxy A" o LO I Y". HTTP Resp onse HTTP response Vojtěch Řehák (Fl MU) Specification and Verification "imers Initiator Responder ICONreq ICON tx- altj -- LATECONF ICONF tY ICONF 1 A OKCONF Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 39 / 97 MSC - Summary Basic MSC 9 instances 9 messages • send events • receive events • conditions 9 coregions • general ordering • inline expressions • time constraints • timers High-level MSC (HMSC) • start node a end node • reference nodes • connection points • lines • conditions • time constraints Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 MSC - Properties • Acyclic property • FIFO property • Race Condition o Deadlock • Livelock • Membership • Nonlocal Choice • Universal Boundedness • Existential Boundedness 9 Time Race Condition • Time Consistency • Tighten Time Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 41 / 97 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 o (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 o (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 2016 42 / 97 MSC - Tools Mesa • academic tool 9 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 Sequence Chart Studio MSC drawing and verification tool developed at Fl MU (Si) File Edit View Insert Format Check Tools Data Shape Window Help □ - Eg a a fliA ^ jt^ax j\*>- a 110% - m ^ Arid j__12pt - I b / U W W m \= iW iW ,A ^ ^ - <3* - [JjJ Theme = - m - *^ - _ Type a question for help Iii.....I"c liftl.....- Search for Shapes: Type your search here v ^ S Co-e=b ^ Be: "* lieft;" ' (Hqhtf T-** Messe O'ce^inc : —i 0"CGrin ■ ■ " 1 . Sizes El « a :^.a, 1 High Level HSC □ X AConnector -\7 Start — Prim I Symbol I AEre r-^-i MSC Symbol l~-r-f FLeference I <4>— I sr™ . I sz^y^— a™ 1:1 i-v.i Clw:: Rate Free ■■iola-ecl.-•; . " Verification failed, Properties violated, Properties to check Name □ : 0 Deadlock Free 0 FIFO 0 LivelockFree 0 Local Choice 0 Race Free < > Display ft r«*ib http: //sestudio.sourceforge.net Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 Distributed vs. Local sdl Specification Description Language msc Message Sequence Chart ITU-T Z.100 It i fait 1 > (Telephone ^ on -I Look J 1 Caller goes off-hook Caller gels ikll KJILI- T j— Language symbols Graphical specification ITU-T Z.120 CmtltiaC'l l'r'-,r]|| t|i,| MAC í Kuknul M«i[|iLnil IlLtlirl Iii rl 1 " II i- AittH'.iflllHltllMH MtTS HAIAiimiiarlii i models of components communication model Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 Specification Description Language (SDL) Specification Description Language (SDL) j Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 46 / 97 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 implemented guide • Z.101 - SDL - Basic SDL-2010 • Z.102 - SDL - Comprehensive SDL-2010 • Z.103 - SDL - Shorthand notation and annotation in SDL-2010 • Z.104 - SDL - Data and action language in SDL-2010 a Z.105 - SDL - SDL-2010 combined with ASN.l modules • Z.106 - SDL - Common interchange format for SDL • Z.108 - SDL - Object-oriented data in SDL-2010 • Z.109 - SDL - UML profile for SDL-2010 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 SDL - Specification Description Language An object oriented languages for specification of applications that a • heterogeneous, 9 distributed (concurrent), • interactive (event-driven, discrete signals), and • real-time dependent (with delays, timeouts). Describes 9 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 2016 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 2016 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 2016 SDL/GR - Process process type diagram. > variables process type Controller 1(1) del cur_panel Pld ^current panel whose Code will be validated 7~ del cid, PIN integer; /* temporary variables for the data attributes of 'Code' 7 start Idle state Validation input CodeicidpiN^ 7* from Panel 7 OK /* from Central 7 ^_task cjr panel := SENDER OK TO cur_paneL Code(cid,PINj TO CentralUnit unlockDoor next state Validati ion )^ Idle unlockDoor procedure reference NOK /* from Central 7 NOK TO cur_paneL procedure call output Idle Vojtěch Řehák (Fl MU) -i li ji i— i _|_i_a y\ Specification and Verification Spring 2016 50 / 97 SDL/GR - Procedure procedure GetPIN fpar in/out pin Integer, IN nodig Integer 1(1) del d Integer; /* digit val je 7 del i Integer; r runner O:no_dig 7 a pin 0 ( Wait Dig it J ^> Digit(d) from Keyboard pin := pin*10 + d I:- i + 1 False ( WaitDigit j .variable procedure "start decision return Vojtěch Řehák (Fl MU) Specification and Verification source: TIMe Electronic Textbook v4.0 Spring 2016 51 / 97 SDL/GR - Block block (type) heading text symbol e [(inp)] [(outpH block type AccessPoint signal opened.closed : /* Door ■> Controller 7 ^~ signal open, close Controller :.- Door V /*signal lists (inp), (out) and (validity) defined in enclosing block. This holds also for signal 'Code' */ 1(1) Controller CE [(inp)] [(outp)] A Panel P1 Controller u [(validity)] [code] [opened, closed] [isOpen, isClosed] D [open, close] [(validity)] CU [Code] signal definitions [isOpen, isClosed] [(validity)] [Code] signal list blocktype diagram signal route cai i vr-d• ~T~i kAa F Icir-\- vr\n ir- Tavt Spring 2016 SDL/GR - Block with block structure block type diagra block (type) heading text A symbol e KirlP)] [(outpH block type AccessPoint 1(1) signal opened,dosed ; /* Door TO Controller V signal open, close ; /* Controller TO Door 7 CEj(inp)] [(outpH A gate signal list Panel Door [(validity) P1 [code; Controller CU [opened, closed^ D [open, close] [(validity)] V [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 2016 53 / 97 SDL/GR - System (the top most block) system AccessControl 1(1) /* Signal definitions for AccessPoint corrirriunication 7 SIGNAL eject-card, lock, unlock input-card, isOpen, isClosed /* ENV display, keys: /* Access Po i nt TO EN V 7 TO Access Point 7 /* Display TO ENV 7 /* ENV TO Keyboard 7 SIGNAL Code (integer, integer);/'Access Point TO GentralUnit 7 SIGNAL QK,NOK,ERR : /* GentralUnit TO AccessPoint 7 SIGNALLIST validity = OK, NOK, ERR ; SIGNALLISToutp = EjectCard, display; SIGNALLIST inp = InputCard, keys ; CE AccessPoint [(outp)] i [(inp)] eAP(10Q): c AccessPoint d [(validity)] [Code] block type (reference) GentralUnit CD [isOpenjsCloset [lock, unlock] signal block set accord- lisl ing to a block type channel block (single) Vojtěch Řehák (Fl MU) Specification and Verification source: TIMe Electronic Textbook v4.0 Spring 2016 54 / 97 SDL/GR - Channels Nondelaying channels for "immediate" message delivery (e.g., between processes within a computer). <-► Delaying channels for "time consuming" message delivery (e.g., between dislocated blocks). -4-►- Channels can also be one-directional. 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 2016 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 signa TD ute SDL Process source: TIMe Electronic Textbook v4.0 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 57 / 97 Asterisk Save, Asterisk State, and Dash State process type heading redefined process type r «block type BlockingAccessPoint» Controller inherits <> Controller BlockDooi Disable BlockDoor blocked Vojtěch Řehák (Fl MU) Enable Idle procedure reference asterisk "state asterisk save procedure call blocked Disable i dash state Specification and Verification source: TIMe Electronic Textbook v4.0 Spring 2016 58 / 97 Timer Construction TIMER door timeout ; set (now +10, door timeout) door timeout set(qj) reset(T) now >= q: Send T-signal to self set(qj); source: TIMe Electronic Textbook v4.0 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 59 / 97 Multiple Instances of a Block system Ac cess Control 1(1} CE AccessPoint [(Outp>][{irlp)] e AP(100): C AccessPoint d [(validity}] [Code] C CentralUnit CD [isO pen, is Closed] [locken lock] source: TIMe Electronic Textbook v4.0 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 60 / 97 Multiple Instances of a Process Block Blockgame SIGNAL Game over (P Gameoverack; [öameover J R4 JBumpJ Monitor (1,1) [Newgame El R5 Bump, Game overack Game(0,) Probe, Result, Endgame R2 R3 Gameid, Win, Score Deamonserver.in D e am an s e rver. out Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 61 / 97 Additional SDL Constructs • Asterisk save, asterisk state, and dash state • Timer construction • Multiple block instances (no dynamic creation) 9 Multiple process instances (with dynamic creation and limit) • Packages collections of related types and definitions (library) • Subtypes • Virtual processes • Process type redefinition and finalization • Inherited blocks Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 SDL - Overview system example_3(3jn ^ system example process p2 2(211 - —" procedure pr 1 (1) (TO C^") P2 > CeD Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 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 2016 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 2016 64 / 97 MSC and SDL in Workflow • typical/optimal communication sequences (MSC) o error sequences (MSC) 9 optionally - full specification in (HMSC) • distributed specification (SDL) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 65 / 97 MSC and SDL in Workflow • typical/optimal communication sequences (MSC) o error sequences (MSC) 9 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 2016 65 / 97 SDL - Tools IBM Rational 9 from tools of Telelogic (SDT, Geode, Tau • 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 J Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 67 /97 Petri Nets C. A. Petri: Kommunikation mit automaten, 1962 Basic components: • places places with tokens inside • transitions • tokens • arcs Marking = configuration = distribution of tokens = vector of #s of tokens in places transition 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 2016 68 / 97 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 transition output places Tokens from input places are removed and new tokens are added into the output places of the fired transition. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 68 / 97 Demonstration Example #1 YellowToRed GreenTüYellow RedToRedyellow RedyellowTüGreen Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 69 / 97 Demonstration Example #1 YellowToRed GreenTüYellow RedToRedyellow RedyellowTüGreen What is wrong in this example? J Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 69 / 97 Demonstration Example #2 Better and a bit more complicated example. red_yellow Vojtěch Řehák (Fl MU) red yellow Specification and Verification Spring 2016 70 / 97 Basic Constructions Sequential execution Alternative Parallel execution Basic Constructions Semaphore Rende-vous Basic Constructions Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 73 / 97 Basic Constructions Basic Constructions Basic Constructions Basic Constructions Critical section Vojtěch Řehák (Fl MU) Alternation Specification and Verification Spring 2016 73 / Basic Constructions Critical section Vojtěch Řehák (Fl MU) Alternation Specification and Verification Deadlock Spring 2016 73 / Different Modifications/Extensions of Petri Nets • Condition-Event Petri nets (C-E PN) • Place-Transition Petri nets (P-T PN) • Coloured Petri nets • Hierarchical Petri nets • Timed Petri nets • Time Petri nets 9 Stochastic Petri nets Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 74 / 97 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 2016 75 / 97 Transition-Place Petri Nets An arbitrary number of tokens in each place producer consumer transp. channel notification channel Producer-consumer model for bounded transport channel. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 Additional Constructs - Arc Multiplicity Additional Constructs - Arc Multiplicity Additional Constructs - Arc Multiplicity Additional Constructs - Arc Multiplicity 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 2016 78 / 97 Additional Constructs - Inhibitor and Reset Arcs Ó 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 2016 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 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 + Pa + Ps + 3 * p6. o t-invariant o an invariant vector on transitions, i.e. a multiset of transitions whose firing leave invariant any marking, e.g. ti + 2 * £2 + £3 + U + £5. p2 t2 p3 Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 80 / Coloured Petri Nets Different colours (classes) of tokens. P q r 3'p+2'q+5'r marking expression, arc expression, transition guard (next slide) Colours usually serves for data type representation. j Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 81 / 97 Coloured Petri Net Example source: http://sciencebloKS.com/Koodmath/2007/10/colored_petri_nets.php Specification and Verification Spring 2016 82 / 97 Hierarchical Petri Nets source: htto://www.eridworkflow.orer/kwferid/ewes-web/ Specification and Verification Spring 2016 83 / 97 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 9 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 2016 84 / 97 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 o 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 I http://cs.au.dk/cpnets/industrial-use/ Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 85 / 97 Queueing theory Queueing theory J Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 86 /97 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 2016 87 / 97 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: Example 30 customers will visit the cash machine in an hour. Each will use it for 1.5 minute on average. 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 2016 87 / 97 Queues and Thier Parameters Generator Queue of customers Servers • inter-arrival time distribution (type of the distribution, rate A, or mean inter-arrival time 1/lambda, other moments . ..) • service time distribution (type of the distribution, rate fi, or mean service time 1/mu, other moments ...) • number of servers • maximal queue length • ... Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 88 / 97 Queue Parameters - Kendall Notation A/S/n/B/K/SD A - inter-arrival 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/oc Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 89 / 97 Queueing Networks Disk 1 Requests RAIDO Disk 2 JoinO -?-> Reply Disk 3 Apache - MaxClients = 100 LoadBalancer Web Server 1 Web Server • open and closed networks • system dependences • traffic intensity • occupancy (on different servers), bottleneck detection, . .. • very similar to Stochastic Petri Nets Questions about Queues • What is the utilization factor p, probability of being not empty? • What is the mean number N of waiting (or being served) requests? • What is the mean waiting and service time, i.e. the time T the requests spends in the system? • And so, how many servers do I need to ... Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 91 Questions about Queues • What is the utilization factor p, probability of being not empty? • What is the mean number N of waiting (or being served) requests? • What is the mean waiting and service time, i.e. the time T the requests spends in the system? • And so, how many servers do I need to ... General solution: • simulation For specific types of queues: o analytical results Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 91 / 97 Analytical Solutions for M/M/l Queues For M/M/l/oc queue with arival rate A and service time rate p\ • The mean inter-arrival time is 1/A. • The mean service time is 1/p. • The utilization factor p — \/p. • The queue is stable if p < 1, i.e. A < p. • The (stable) queue is empty with probability Pq — 1 — p. • The mean number of requests (waiting or being served) in a stabl system N — p/{l — p). It is also usually denoted by L as it is the length of the queue. • The average time spend in a stable system T = l/(M-A) = l/(/i(l-p)). • The rate of the trafic carried out by the queue is pp = p(l — Po). Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 Our Motivation Example Solved as M/M/l/oc ixample 30 customers will visit our cash machine in an hour. Each will use it for 1.5 minute on average. How busy is the cash machine? What is the average waiting time? Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 93 / 97 Our Motivation Example Solved as M/M/l/oc ixample 30 customers will visit our cash machine in an hour. Each will use it for 1.5 minute on average. How busy is the cash machine? What is the average waiting time? • The mean inter-arrival time is 2 minutes. • The rate of the inter-arrival time A is 1/2 = 0.5. • The mean service time is 1.5 minute. • The rate of the service time n is 2/3 ~ 0.666667. • The queue is stable and the utilization factor p — 3/4 = 0.75. • The mean number of requests (waiting or being served) N is 3. • The average time spend in the system T is 6 minutes. I.e., the utilization of the cash machine is 45 minutes in an hour, i.e. 75%. Average number of customers at the cash machine is 3. The average waiting of a customer is 4.5 minutes + 1.5 min for service. Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 93 / 97 Little's Law Theorem Let L be the long-term average number of customers in a stable system, A be the long-term average effective arrival rate, and W be the average time a customer spends in the system. Then it holds that L = A- W for a queue of any type. 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." Specification and Verification Spring 2016 94 / Tools for Queueing Systems G/M/c-like queue • online steady-state solution of a G/M/c-like queue 9 http://queueing-systems.ens-lyon.fr/formGMC.php Queueing Simulation • online queueing network analyzer 9 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) a http://www.mathworks.com/products/simevents/ Up-to-date List of relevant Queueing theory based tools: ^^^^l^^j^//web^^iwmdsor^ Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 95 / 97 Relevant Lectures IV113 Uvod do validace a verifikace (Barnat) IA169 System Verification and Assurance (Barnat, Řehák, Matyáš) IV109 Modelovania simulace (Pelánek) IA159 Formal verification methods (Strejček) IA158 Real Time Systems (Brázdil) Vojtěch Řehák (Fl MU) Specification and Verification Spring 2016 96 / 97 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. • 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ě. VSB - 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 2016 97 / 97