FACULTY OF INFORMATICS Masaryk University PA160: Net-Centric Computing II. Specification and Verification of Network Protocols Vojtěch Řehák Spring 2023 This presentation is not a self-contained study material. It is strongly recomended to attend the lecture or watch the records. Vojtěch Řehák • Specification and Verification • Spring 2023 1/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage Theory Vojtěch Řehák • Specification and Verification • Spring 2023 2/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage Vojtěch Řehák • Specification and Verification • Spring 2023 2/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage T Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University Theoretical Results as Tools for Users Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 4/96 FACULTY OF INFORMATICS I Masaryk University Formal Models in Specification natural Language vs. formal Language freedom in writing © © restrictions in writing human resources © © automatic methods Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 5/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 5/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 5/96 FACULTY OF INFORMATICS Masaryk University Map - Abstraction Example Find Pardubice or directions from Brno to Liberec. Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University Map - Abstraction Example r Find Pardubice or directions from Brno to Liberec. source: www.mapy.cz Vojtěch Řehák • Specification and Verification • Spring 2023 6/96 FACULTY OF INFORMATICS Masaryk University Map - Abstraction Example "Model has to suit its purpose!" Only relevant information are presented; no more, no Less. Vojtěch Řehák • Specification and Verification • Spring 2023 6/96 FACULTY OF INFORMATICS Masaryk University Outline Models we will talk about: ■ Message Sequence Charts (MSC) ■ Specification and Description Language (SDL) ■ Petri nets ■ Oueueing theory What they can be used for? ■ modelling ■ specification ■ analysis ■ simulation ■ testing ■ partial implementation Vojtěch Řehák • Specification and Verification • Spring 2023 7/96 FACULTY OF INFORMATICS Masaryk University Distributed Systems "What is the problem of distributed systems?" J Vojtěch Řehák • Specification and Verification • Spring 2023 8/96 FACULTY OF INFORMATICS Masaryk University Distributed Systems World is distributed Vojtěch Řehák • Specification and Verification • Spring 2023 9/96 FACULTY OF INFORMATICS Masaryk University Distributed Systems World is distributed Human way of thinking is sequential Vojtěch Řehák • Specification and Verification • Spring 2023 9/96 FACULTY OF INFORMATICS Masaryk University Distributed vs. Local SDL MSC Specification Description Message Sequence Language Chart ITU-T Z.100 ITU-T Z.120 Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University Distributed vs. Local SDL Specification Description Language MSC Message Sequence Chart input Output ITU-T Z.100 CTelephon« ^ or-hook J ~r > Caller bow off'hook Caller gers Jul [um- t Dial töne JJ J 1 Cr aphlca] specification ITU-T Z.120 Cmtltiali.il lirsrlillh'l n.| lI Uttip En* ÍI lI 11(51 IlLtlirl 111 rl 11. n MÍTS iJATt'nilfllPl i- .Vkh„»lr Caller bow off'hook Caller gers Jul [um- t Dial toňě JJ J 1 Cr aphlctd specification ITU-T Z.120 (X ttllniliil lirsr 111 Cll-rl n.| lI ÍI lI iittlliUltti Iii rl 11, n nlCI^DATiUtqiinl MÍTS iJATtrniifliin i- AiknuMilnltiiMii Mi EMI M V null.,Ii hi modeLs of components communication model Vojtěch Řehák • Specification and Verification • Spring 2023 44/96 FACULTY OF INFORMATICS Masaryk University Specification Description Language (SDL) Specification Description Language (SDL) J Vojtěch Řehák • Specification and Verification • Spring 2023 45/96 FACULTY OF INFORMATICS Masaryk University 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 ■ ... ■ 06/2021 - 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 ■ 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 ■ ... Vojtěch Řehák • Specification and Verification • Spring 2023 46 / 96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 47/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 48/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 48/96 FACULTY OF INFORMATICS Masaryk University SDL/GR - Process process type diagram. variables process type Controller 1(1) del cur_panel Pld ^current panel whose Code will be validated "1 del cid PIN integer : /* temporary variables for the data attributes of Code 7 stale Idle state input Validation xNCode(cid.PIN^ >tronri Panel V OK /* from Central 7 __task cur panel := SENDER OK TO cur_panel- Code(cid,PiN)>- TO CentralUnit unlockDoor I next st ate Validatio 1/ I Idle unlockDoor procedure reference NOK /* from Central 7 NOK TO cjr_paneL procedure call output Idle Vojtěch Řehák • Specification and Verification • Spring 2023 source: TIMe Electronic Textbook v4.0 49/96 FACULTY OF INFORMATICS Masaryk University SDL/GR - Procedure procedure GetPIN fpar in/out pin Integer, IN no_dig Integer del d Integer; /* digit value 7 del i Integer; /* runnerO:no_dig * CO) pin := 0 i :=0 ( WaitDigit ^ Digit(d) 1(1) from Keyboard pin := pin*10 + d i :=i + 1 False ^ WartPigit ^ .variable proceduro start decision re lu in Vojtěch Řehák • Specification and Verification • Spring 2023 source: TIMe Electronic Textbook v4.0 50/96 FACULTY OF INFORMATICS Masaryk University SDL/GR - Block block (type) heading text x symbol signal opened,dosed ; /* 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' 7 [(inp}] [(ojtpH block type AccessPoint 1(1) CE [(inp)] [(outp)] i PI [(validity)] [code] rilock, jock] [isOpen, isClosed] Controller u [opened, closed] D [open, close] [(validity)] CU [Code] signal definitions -process type process I unlock, lock] |isC)pen, isClosed] [(validity)] [Code] signal list / blocktype diagram ig nal route source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2023 51/96 FACULTY OF INFORMATICS Masaryk University SDL/GR - Block with block structure block type diagran text symbol e KinpH [(outpH block (type) heading block type AccessPoint 1(1) signal opened,closed ; /* Door TO Controller 7 Signal open, close ; /* Controller TO Door */ signal definitions CE [(inp)] [(outpH 4 Panel Door [(validity) P1 [code Controller CU [opened, closed] D [°Per1> close] [(validity)] V [Code] C [Code] [(validity)] gate Signal list block (single) channel source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2023 52/96 FACULTY OF INFORMATICS Masaryk University SDL/GR - System (the top most block) system Access Control 1(1) /* Signal definitions for Access Point communication 7 SIGNAL ejects a rd, lock, unlock /* Access Point TO ENV 7 input-Card, isOpen, isClosed /* ENV TO AccessPoint7 display, /* Display TO ENV 7 keys; /*ENV TO Keyboard 7 SIGNAL Code (integer,int€jger);/* Access Point TO CentralUnit 7 SIGNAL OK,NOK,ERR ; /* CentralUnit TO AccessPoint 7 SIGNALLIST validity = OK, NOK, ERR ; SIGNALLISToutp = EjectCard, display; SIGNALLIST imp = InputCard, keys ; CE AccessPoint block type (reference) [(outp)] 1 KinpH LaP(100): c [(validity}] [Code] CentralUnit , AccessPoint 4 d ' 4 c CD [isOpenjsCloset [lock, unlock] signal block set accord-list ing to a block type i channel block (single) source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2023 53/96 FACULTY OF INFORMATICS Masaryk University 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). <—► Channels can also be one-directional. Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 55/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 source: TIMe Electronic Textbook v4.0 56/96 FACULTY OF INFORMATICS Masaryk University Asterisk Save, Asterisk State, and Dash State process type heading redefined process type «block type BlockingAccessPoint>> Controller inherits <> Controller BlockDooi Disable BlockDoor Í blocked blocked Enable Idle procedure reference asterisk "state asterisk save procedure call blocked Disable I dash state source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2023 57/96 FACULTY OF INFORMATICS Masaryk University Timer Construction TIMER door timeout set(qj); Vojtěch Řehák • Specification and Verification • Spring 2023 source: TIMe Electronic Textbook v4.0 58/96 FACULTY OF INFORMATICS Masaryk University Multiple Instances of a Block sy stem Access Control 1(1} CE Access Point [(outpH KlnpJ] e AP(100): c Access Point d I [(validity}] [Code] GentralUnit [isO pen, is Closed] [locken lock] source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2023 59/96 FACULTY OF INFORMATICS Masaryk University Multiple Instances of a Process Newgame Game I Block Blockgame SIGNAL Game aver (P; Gameoverack Rj JGameover J R4 jßumpj [blewgame J Bump, Gameoverack f~ s. r~ v. Monitor (1,1) h Game(0,) V \ V_ / Probe, Result, Endgame R2 R2i Gameid, Win, Lost, Score Deamonserver.in Deamonserver.out Vojtěch Řehák • Specification and Verification • Spring 2023 60/96 FACULTY OF INFORMATICS I Masaryk University 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 ■ Process type redefinition and finalization ■ Inherited blocks Vojtěch Řehák • Specification and Verification • Spring 2023 61/96 FACULTY OF INFORMATICS Masaryk University SDL - Overview . system eaarrsle system example Systems ami blocks ct&i contain blocks anaYorprocesses. Processes contain j behaviour and cannot contain blocks. procedure pr 1 (1) (El Vojtěch Řehák • Specification and Verification • Spring 2023 62/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 63/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 63/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 64/96 FACULTY OF INFORMATICS Masaryk University 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)MSCto SDL transformation (realization) ■ SDL to source code transformation (implementation) ■ MSC to test case transformation ■ simulation to MSC transformation (membership checking) Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS I Masaryk University SDL - Tools IBM Rational ■ 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 • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University Petri Nets Petri Nets J Vojtěch Řehák • Specification and Verification • Spring 2023 66/96 FACULTY OF INFORMATICS Masaryk University Petri Nets C.A. Petri: Kommunikation mit automaten, 1962 Basic components: ■ places ■ transitions ■ tokens ■ arcs Marking = configuration = distribution of tokens = vector of token #s in places places with tokens inside transition A transition can be fired if there is a token in each of its input places. Vojtěch Řehák • Specification and Verification • Spring 2023 67/96 FACULTY OF INFORMATICS Masaryk University Petri Nets C.A. Petri: Kommunikation mit automaten, 1962 Basic components: ■ places ■ transitions ■ tokens ■ arcs Marking = configuration = distribution of tokens = vector of token #s 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 • Specification and Verification • Spring 2023 67/96 FACULTY OF INFORMATICS Masaryk University Demonstration Example #1 YellowToRed GreenToYellow RedToRedyellow RedyellowToGreen Vojtěch Řehák • Specification and Verification • Spring 2023 68/96 FACULTY OF INFORMATICS Masaryk University Demonstration Example #1 YellowToR GreenToYell Vojtěch Řehák • Specification and Verification • Spring 2023 68 / 96 FACULTY OF INFORMATICS Masaryk University Demonstration Example #2 Better and a bit more complicated example. red_yellow yellow_red Vojtěch Řehák • Specification and Verification • Spring 2023 69 / 96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Sequential execution Iteration Alternative Parallel execution Vojtěch Řehák • Specification and Verification • Spring 2023 70/96 FACULTY OF INFORMATICS I Masaryk University Basic Constructions Semaphore Rende-vous Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University Basic Constructions Vojtěch Řehák • Specification and Verification • Spring 2023 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Vojtěch Řehák • Specification and Verification • Spring 2023 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Vojtěch Řehák • Specification and Verification • Spring 2023 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Alternation Vojtěch Řehák • Specification and Verification • Spring 2023 72/96 FACULTY OF INFORMATICS Masaryk University Critical section Alternation Vojtěch Řehák • Specification and Verification • Spring 2023 72/96 FACULTY OF INFORMATICS Masaryk University Critical section Alternation Vojtěch Řehák • Specification and Verification • Spring 2023 Deadlock 72/96 FACULTY OF INFORMATICS Masaryk University 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 ■ Stochastic Petri nets Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2023 74/96 FACULTY OF INFORMATICS Masaryk University Transition-Place Petri Nets An arbitrary number of tokens in each place. producer notification channel Producer-consumer model for bounded transport chan Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity Vojtěch Řehák • Specification and Verification • Spring 2023 76/96 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity Vojtěch Řehák • Specification and Verification • Spring 2023 76/96 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity 3 Vojtěch Řehák • Specification and Verification • Spring 2023 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Inhibitor and Reset Arcs An inhibitor arc imposes the precondition that the transition may only fire when the place is empty. Vojtěch Řehák • Specification and Verification • Spring 2023 77/96 FACULTY OF INFORMATICS Masaryk University Additional Constructs - An inhibitor arc imposes the precondition that the transition may only fire when the place is empty. ibitor and Reset Arcs A reset arc does not impose a precondition on firing, and empties the place when the transition fires. Vojtěch Řehák • Specification and Verification • Spring 2023 77/96 FACULTY OF INFORMATICS Masaryk University 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 FACULTY OF INFORMATICS Masaryk University 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 * p1 + p2 + Pi + Pa + Ps + 3 * p6- ■ t-invariant ■ an invariant vector on transitions, i.e. a multiset of transitions whose firing leave invariant any marking, e.g. fl + 2*f2+f3+f4 + f5. p2 t2 P3 Vojtěch Řehák • Specification and Verification • Spring 2023 79/96 FACULTY OF INFORMATICS Masaryk University Coloured Petri Nets Different colours (classes) of tokens. P q r 3'p+2q+5'r marking expression, arc expression, transition guard (next slide) Colours usually serves for data type representation. Vojtěch Řehák • Specification and Verification • Spring 2023 80/96 FACULTY OF INFORMATICS Masaryk University Coloured Petri Net Example Vojtěch Řehák • Specification and Verification • Spring 2023 81/96 FACULTY OF INFORMATICS Masaryk University Hierarchical Petri Nets Vojtěch Řehák • Specification and Verification • Spring 2023 82/96 FACULTY OF INFORMATICS I Masaryk University 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 • Specification and Verification • Spring 2023 83/96 FACULTY OF INFORMATICS Masaryk University PN Tools CPN Tools ■ Coloured Petri Nets (prioritized transitions and realtime support) ■ editor, simulation, analyses Tapall ■ Timed-Arc Petri Nets (with realtime 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,... http://wwwjnformatik.uni-hamburg.de/TGI/PetriNets/tools/quick.html http://cs.au.dk/cpnets/industrial-use/ Vojtěch Řehák • Specification and Verification • Spring 2023 84/96 FACULTY OF INFORMATICS Masaryk University Oueueing theory Oueueing theory J Vojtěch Řehák • Specification and Verification • Spring 2023 85/96 FACULTY OF INFORMATICS Masaryk University Oueueing 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 • Specification and Verification • Spring 2023 86/96 FACULTY OF INFORMATICS I Masaryk University Oueueing 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 cash machine in an hour. Each customer uses the machine 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 • Specification and Verification • Spring 2023 86/96 FACULTY OF INFORMATICS Masaryk University 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/A, other moments ...) ■ service time distribution (type of the distribution, rate /i, or mean service time 1///, other moments ...) ■ number of servers ■ maximal queue Length ■ ... Vojtěch Řehák • Specification and Verification • Spring 2023 87/96 FACULTY OF INFORMATICS Masaryk University Queue Parameters - Kendall Notation A/S/n/B/K/SD A - inter-arrivaL time distribution G - general, M - exponential, 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 • Specification and Verification • Spring 2023 88 / 96 FACULTY OF INFORMATICS Masaryk University Oueueing Networks Requests RAIDO Disk 1 Disk 2 JoinO Disk 3 Reply Apache - MaxClients = 100 LoadBalancer 3 Web Server 1 jH Web Server 2 open and closed networks system dependences traffic intensity occupancy (on different servers), bottleneck detection, very similar to Stochastic Petri Nets Vojtěch Řehák • Specification and Verification • Spring 2023 89/96 FACULTY OF INFORMATICS Masaryk University 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 spend in the system? ■ And so, how many servers do I need to ... Vojtěch Řehák • Specification and Verification • Spring 2023 90/96 FACULTY OF INFORMATICS Masaryk University 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 spend in the system? ■ And so, how many servers do I need to ... General solution: ■ simulation For specific types of queues: ■ analytical results Vojtěch Řehák • Specification and Verification • Spring 2023 90/96 FACULTY OF INFORMATICS I Masaryk University 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///. ■ The utilization factor p = X/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 stable 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/(p - A) = 1/(M(1 - p)). ■ The rate of the trafic carried out by the queue is pp = p(l - Pq). Vojtěch Řehák • Specification and Verification • Spring 2023 91/96 FACULTY OF INFORMATICS Masaryk University Our Motivation Example Solved as M/M/l/oc Example 30 customers will visit our cash machine in an hour. Each customer uses the machine for 1.5 minute on average. How busy is the cash machine? What is the average waiting time? Vojtěch Řehák • Specification and Verification • Spring 2023 92/96 FACULTY OF INFORMATICS Masaryk University Our Motivation Example Solved as M/M/l/oc Example 30 customers will visit our cash machine in an hour. Each customer uses the machine 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 p 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., on average: It serves 45 minutes per hour. There are 3 customers in the queue and each spends 4.5 minutes for waiting + 1.5 min for service. Vojtěch Řehák • Specification and Verification • Spring 2023 92/96 FACULTY OF INFORMATICS Masaryk University Little's Law Theorem Let L be the long-term average number of customers in a stable system, X 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." Vojtěch Řehák • Specification and Verification • Spring 2023 93/96 FACULTY OF INFORMATICS Masaryk University Tools for Oueueing Systems G/M/c-like queue ■ online steady-state solution of a G/M/c-Like queue ■ https://queueing-systems.ens-lyon.fr/formGMC.php 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 Oueueing theory based tools: http://web2.uwindsor.ca/math/hlynka/qsoft.html Vojtěch Řehák • Specification and Verification • Spring 2023 94/96 FACULTY OF INFORMATICS Masaryk University Relevant Lectures IA169 System Verification and Assurance (Barnat, Řehák, Matyáš) IV109 Modelování a simulace (Pelánek) IA159 Formal verification methods (Strejček) IA158 Real-Time Systems (Brázdil) (to appear) Algorithms for Quantitative Verification (J. Křetínský) (to appear) Model Checking (Strejček, Jonáš) (to appear) Satisfiability and Automated Reasoning (Jonáš) Vojtěch Řehák • Specification and Verification • Spring 2023 95/96 FACULTY OF INFORMATICS I Masaryk University References ■ ITU-T recommendation Z.120: Message Sequence Charts (MSC). 2011. ■ ITU-T recommendation Z.100: Specification Description Language (SDL). 2019. ■ S. Mullender. Distributed Systems. ACM, 1993. ■ D. PeLed. Software Reliability Methods. Springer, 2001. ■ R. Braek at a I. TIMe: The Integrated Method. SINTEF, 1999. ■ L. DoLdi. Validation of Communications Systems with SDL. WiLey, 2003. ■ M. Broy and K. Stolen. 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 site. Akademické nakladatelství CERM Brno, 1994. ■ J. Markl. Petriho site. 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 • Specification and Verification • Spring 2023 96/96