FACULTY OF INFORMATICS Masaryk University PA160: Net-Centric Computing II. Specification and Verification of Network Protocols Vojtěch Řehák Spring 2020 This presentation is not a self-contained study material. It is strongly recomended to watch the video records from Spring 2019. Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 1/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage Theory Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. 2/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage 2/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage 2/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage 2/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage 2/96 FACULTY OF INFORMATICS Masaryk University Theoretical Results as Tools for Users Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 3/96 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 2020 This presentation is not a self-contained study material. It is 4/96 FACULTY OF INFORMATICS I Masaryk University Formal Models in Specification natural Language vs. formal Language freedom in writing O Q restrictions in writing human resources © © automatic methods Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. 5/96 FACULTY OF INFORMATICS Masaryk University Formal Models in Specification natural Language vs. formal Language freedom in writing O Q 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 2020 This presentation is not a self-contained study material. 5/96 FACULTY OF INFORMATICS Masaryk University Formal Models in Specification natural Language vs. formal Language freedom in writing O Q 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 2020 This presentation is not a self-contained study material. 5/96 FACULTY OF INFORMATICS Masaryk University Formal Models in Specification natural Language vs. formal Language freedom in writing O Q 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 2020 This presentation is not a self-contained study material. 5/96 FACULTY OF INFORMATICS Masaryk University Map - Abstraction Example Find Pardubice or directions from Brno to Liberec. ^Iirrp.wwwm3nvr7 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a s^T-^órrtaWa ytddyrriateriaL It is 6/96 FACULTY OF INFORMATICS Masaryk University Map - Abstraction Example Find Pardubice or directions from Brno to Liberec. ^Iirrp.wwwm3nvr7 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a selT-^oinatn^a-siuByrnateriaL It is 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 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 7/96 FACULTY OF INFORMATICS Masaryk University Distributed Systems "What is the problem of distributed systems?" Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 8/96 FACULTY OF INFORMATICS Masaryk University Distributed Systems nd Verification • Spring 2020 This presentation is not a self-contained study material. 9/96 FACULTY OF INFORMATICS Masaryk University Distributed Systems W^dl&JMntlLd Verification . Sprin&lMsWYnßfio^s«& 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 2020 This presentation is not a self-contained study material. It is 10/96 FACULTY OF INFORMATICS Masaryk University Distributed vs. Local SDL Specification Description Language MSC Message Sequence Chart i'Mif input Output ITU-T Z.100 CTeleptiůní or-hook J ~r > Caller bow off-hook jL Caller^ei Jul [um- t 1^ Dial tOňČ 1 Gr aphfca] specification ITU-T Z.120 Cmtltiali.il iwxlliltlm Iii rl '.1 lI JI lI llll llNtl'l 11, n iKPS DAT.VfMufowi i- ^rt(,iiM|lH|íJllr(l! MritiHAJAjiMllnirl.i i models of components communication model Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 10/96 FACULTY OF INFORMATICS Masaryk University Message Sequence Chart (MSC) Message Sequence Chart (MSC) J Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 11/96 FACULTY OF INFORMATICS Masaryk University 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 ■ 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 • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 12/96 FACULTY OF INFORMATICS Masaryk University 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 ■ 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 • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 12/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 13/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 14/96 FACULTY OF INFORMATICS Masaryk University Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 15/96 FACULTY OF INFORMATICS I Masaryk University Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 15/96 FACULTY OF INFORMATICS I Masaryk University Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. 15/96 FACULTY OF INFORMATICS I Masaryk University Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. 15/96 FACULTY OF INFORMATICS I Masaryk University MSC - Visual Order Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. 16/96 FACULTY OF INFORMATICS I Masaryk University MSC - Visual Order - Hasse Diagram Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. 17/96 FACULTY OF INFORMATICS Masaryk University MSC Properties What is an unwanted behaviour/property? Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 18/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 18/96 FACULTY OF INFORMATICS Masaryk University Acyclic/Cyclic property cyclic dependency among events Instance p Instance q unrealizable in any environment Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 19/96 FACULTY OF INFORMATICS Masaryk University Acyclic/Cyclic property Client Manager Software Architect Make a product Make a product Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 20/96 FACULTY OF INFORMATICS Masaryk University FIFO/non-FIFO property overleaping messages Instance p Instance q Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 21/96 FACULTY OF INFORMATICS Masaryk University FIFO/non-FIFO property overleaping messages Instance p Instance q unrealizable in an environment preserving message order Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 21/96 FACULTY OF INFORMATICS Masaryk University FIFO/non-FIFO property overleaping messages Instance p Instance q Instance p Instance q Instance r m2 ---► m3 <4- unrealizable in an environment preserving message order Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 21/96 FACULTY OF INFORMATICS Masaryk University 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 I tZoftSdi ^hORQ^^toijQill Cil394frfft@t|lon • Spring 2020 This presentation is not a self-contained study material. It is 21/96 FACULTY OF INFORMATICS Masaryk University Race Condition Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 22/96 FACULTY OF INFORMATICS Masaryk University Race Condition Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. 22/96 FACULTY OF INFORMATICS Masaryk University Race Condition Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. 22/96 FACULTY OF INFORMATICS Masaryk University Solution #1 - Coregion Construction Let us demonstrate that some events are not ordered. Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 23/96 FACULTY OF INFORMATICS Masaryk University Solution #1 - Coregion Construction Let us demonstrate that some events are not ordered. Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 23/96 FACULTY OF INFORMATICS Masaryk University Solution #1 - Coregion Construction Let us demonstrate that some events are not ordered. Peter Jane Paul Events in a coregion are not ordered; except for the event related by general ordering. Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 23/96 FACULTY OF INFORMATICS Masaryk University Solution #2 - List/set of all possibilities Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 24/96 FACULTY OF INFORMATICS Masaryk University Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 25/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 msc ACsystemOverview connection point if-f HMSC start Idle ^4oop User accepted < Door unlocked Unlocked reset User rejected T msc reference restrictive condition Unlocked timeout Unlocked unclosed alternative Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 26/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 \7 Trace example: Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 c r 1 1 i > Trace example: Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Trace example: Vojtěch Řehák • Specification and Verification • Spring 202thffiiSTJres¥ififl?o$i Sfíot PsQÍf-íoli(Ím&řílády material. It is 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 c r 1 1 i > Trace example: Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 1 I Trace example: Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Trace example: A Vojtěch Řehák • Specification and Verification • Spring 2020 27/96 This presentation is not a self-contained study material. It is FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Trace example: Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 27/96 FACULTY OF INFORMATICS Masaryk University Deadlock Property Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 28/96 FACULTY OF INFORMATICS Masaryk University Livelock Property £ Í B Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 29/96 FACULTY OF INFORMATICS Masaryk University Membership Is a given MSC included in a given HMSC? Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 30/96 FACULTY OF INFORMATICS Masaryk University Membership Is a given MSC included in a given HMSC? Instance A Instance B 1 1 1__J P . w Input BMSC bMSC01 1 f bMSC02 J Input HMSC Instance A Instance B [ _ 1 1 P bMSCOl Instance A Instance B q bMSC02 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 30/96 FACULTY OF INFORMATICS Masaryk University Inline Expressions System 1 System2 System3 ■ "i i ~i i , ~i altj *----^^Upt ------Stop_____ ^--Qätinue^^ —" I _I I ——1 I _1 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 31/96 FACULTY OF INFORMATICS Masaryk University Inline Expressions System 1 System2 System3 ■ "i i ~i i , ~i altj *----^^Upt ------Stop_____ ^--Qätinue^^ —" I _I I ——1 I _1 Other inline expression types: opt, loop(/77, n), exc, seq, par. Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 31/96 FACULTY OF INFORMATICS Masaryk University Non-local Choice System 1 System2 System3 altj -----íi^mipt --- I "I I "I I 1 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 32/96 FACULTY OF INFORMATICS Masaryk University Non-local Choice System 1 System2 System3 altj -----íi^mipt --- I "I I "I I 1 System3 does not know which alternative has been chosen. J Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 32/96 FACULTY OF INFORMATICS Masaryk University Non-local Choice System 1 System2 System3 ■ "i i , ~i i , ~i altj I I I I I —I Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 32/96 FACULTY OF INFORMATICS Masaryk University Non-local Choice System 1 System2 System3 ■ "i i , ~i i , ~i altj I I I I I —I System3 does not know which alternative has been chosen. J Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 32/96 FACULTY OF INFORMATICS Masaryk University Universal Boundedness What is the size of input buffer of Y that will never overflow? Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 33/96 FACULTY OF INFORMATICS I Masaryk University 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 • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 33/96 FACULTY OF INFORMATICS Masaryk University Universal Boundedness What is the size of input buffer of Y that will never overflow? Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 33/96 FACULTY OF INFORMATICS Masaryk University Universal Boundedness What is the size of input buffer of Y that will never overflow? M M Buffers of size 1 will never overflow. j Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 33/96 FACULTY OF INFORMATICS Masaryk University 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 • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 34/96 FACULTY OF INFORMATICS Masaryk University 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. i sentation is not a self-contained study material. It is 3tei 34/96 FACULTY OF INFORMATICS Masaryk University Race Condition - Solution #3 - Time Constraints Client Proxy Application server agister Message ~~~~~~ ——► Response Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 35/96 FACULTY OF INFORMATICS Masaryk University Race Condition - Solution #3 - Time Constraints Client Proxy Application server Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 35/96 FACULTY OF INFORMATICS Masaryk University Race Condition - Solution #3 - Time Constraints Client Proxy Application server A" c LO agister Message er Response Response "A CO cnT Vojtěch Řehák • Specification and Verification • Spring 2020 35/96 This presentation is not a self-contained study material. It is FACULTY OF INFORMATICS Masaryk University Time Consistency Are the given time conditions consistent? Client A Proxy Server 36/96 FACULTY OF INFORMATICS Masaryk University Time Tightening Some time conditions can be tightened. Client A Proxy Server 37/96 FACULTY OF INFORMATICS Masaryk University Time Tightening Some time conditions can be tightened. Client A Proxy Server 37/96 FACULTY OF INFORMATICS Masaryk University Timers Initiator Vojtěch Řehák • Specification and Responder ICONreq ICON tX- altj tX-► LATECONF ICONF ICONF tY 1 A OKCONF g 2020 This pre elf-contained study material. It is 38/96 FACULTY OF INFORMATICS Masaryk University MSC - Summary Basic MSC ■ instances ■ messages ■ send events ■ receive events ■ conditions ■ coregions ■ general ordering mime expressions time constraints timers High-level MSC (HMSC) ■ start node ■ end node ■ reference nodes ■ connection points ■ Lines ■ conditions ■ time constraints Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 39/96 FACULTY OF INFORMATICS Masaryk University MSC - Properties ■ Acyclic property ■ FIFO property ■ Race Condition ■ Deadlock ■ LiveLock ■ Membership ■ NonLocaL Choice ■ Universal Boundedness ■ Existential Boundedness ■ Time Race Condition ■ Time Consistency Vojtjph"p^hj)^^|^cTpj:p^(gn and Verification • Spring 2020 This presentation is not a self-contained study material. It is 40/96 FACULTY OF INFORMATICS I Masaryk University 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. Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 41/96 FACULTY OF INFORMATICS I Masaryk University 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 • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 41/96 FACULTY OF INFORMATICS Masaryk University 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 VojtRhfe!^^£^Specif^^ is not a self-contained study material. It is 42/96 FACULTY OF INFORMATICS Masaryk University Sequence Chart Studio MSC drawing and verification tool developed at Fl MU. □ X iEjjl) File Edit View Insert Format Check Tools Data Shape Window Help Type a question fb- - _ fi" x Page 2/2 http://scstudio.sourceforge.net Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 43/96 FACULTY OF INFORMATICS Masaryk University Distributed vs. Local SDL Specification Description Language MSC Message Sequence Chart i'Mif input Output ITU-T Z.100 CTelephon« or-hook J ~r > Caller bow off-hook jL Caller^ei Jul [um- t 1^ Dial tOňČ 1 Gr aphfca] specification ITU-T Z.120 Cmtltiali.il iwxlliltlm Iii rl '.1 lI JI lI llll llNtl'l 11, n iKPS DAT.VfMufowi i- ^rt(,iiM|lH|íJllr(l! MritiHAJAjiMllnirl.i i models of components communication model Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 44/96 FACULTY OF INFORMATICS Masaryk University Specification Description Language (SDL) Specification Description Language (SDL) J Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 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 ■ ... ■ 04/2016 - 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 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 48/96 FACULTY OF INFORMATICS Masaryk University SDL/GR - Process process type diagram. variables process type Controller 1(1) del cur_panel Pld urrent panel whose Code will be validated *F~ del cid, PIN integer; /* temporary variables for the data attributes of 'Code' 7 start Idle statt.' input Validation unloekDoor^ procedure reference ^ode(cid,PIN^, "rtrpm Panel V OK /* from Central 7 NOK /* from Central "/ cur_panel := SENDER _task OK \ TO cur paneL NOK TO cur_paneL Code(cid,PIN] TO CentralUnit jnlockDoor next st ate Validatio I procedure \^ call output Idle Idle source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 49/96 FACULTY OF INFORMATICS Masaryk University SDL/GR - Procedure procedure GetPIN fpar in/out pin Integer, IN no_dig Integer del d Integer; del i Integer ; /'digitvalue 7 /* runner O:no_dig */ CO) pin i := := 0 , 0 ^ waitDigit ^ Digit(d) 1(1) from Keyboard pin := pin*10 + d i :=i + 1 False ^ WaitDigit ^ .variable procedure start decision i e in in source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 50/96 FACULTY OF INFORMATICS Masaryk University SDL/GR - Block block (type) heading text symbol [(ojtpH block type AccessPoint 1(1) signal opened,dosed ; /* Door -> Controller */ Signal open, dose ;/* Controller -> Door 7 /* signal lists (inp), (out) and (validity) defined in enclosing block. This holds also for signal 'Code' V signal definitions [Code] signal list blocktype diagram signal route source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 51/96 FACULTY OF INFORMATICS Masaryk University SDL/GR - Block with block structure block type diagran text symbol KinpH [(outp)] k block (type) heading block type AccessPoint 1(1) signal opened,closed ; /* Door TO Controller*/, signal open, close ; /* Controller TO Door */ signal CEjK^p)] A Panel Door L(validity) P1 [code Controller CU [opened, clc^sed^ D [open, close] [(validity)] W [Code] definitions C [Code] [(validity}] gate signal list block (single) channel Vojtěch Řehák • Specification and Verification • Spring 2020 52/96 source: TIMe Electronic Textbook v4.0 This presentation is not a self-contained study material. It is FACULTY OF INFORMATICS Masaryk University SDL/GR - System (the top most block) system Access Control 1(1) /* Signal definitions for AccessPoint communication 7 SIGNAL eject-card, lock, unlock /* AccessPoint TO ENV 7 input-card, isOpen, isClosed r ENV TO AccessPoint7 display, /* Display TO ENV 7 keys; r ENV TO Keyboard 7 SIGNAL Code (integer, integer);/* AccessPoint TO Central Unit 7 SIGNAL OK,NOK,ERR ; /* CentralUnit TO AccessPoint 7 SIGNALLIST validity = OK, NOK, ERR ; SIGNALLISToutp = EjectCard, display; SIGNALLIST inp = InputCard, keys ; CE AccessPoint block rype (reference) L(outp)] 1 [(inp)] eAP(100): c AccessPoint d [(validity)] [Code] - 4 c" CentralUnit CD] [isOpenJsClosei [lock, unlock] signal block set accord- i list ing to a block type chamiel block (single) w « -~ ^- ... *. . r. . . source: TIMe Electronic Textbook v4.0^ Vojtech Rehak • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. 54/96 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 2020 This presentation is not a self-contained study material. It is 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 source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 56/96 FACULTY OF INFORMATICS Masaryk University Asterisk Save, Asterisk State, and Dash State process type heading redefined process type r «block type BlockintjAccessPoint>> Controller inherits < Controller 1 BlockDeoi Disable BlockDoor Í 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 2020 This presentation is not a self-contained study material. It is 57/96 FACULTY OF INFORMATICS Masaryk University Timer Construction TIMER door timeout set(q?T); source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 58/96 FACULTY OF INFORMATICS Masaryk University Multiple Instances of a Block system Access Control 1(1} Access Point [(outpH [(inp)] e AP(100): C AccessPoint d [(validity}] [Code] C GentralUnit CD [isO pen, is Closed] [lock.urilock] source: TIMe Electronic Textbook v4.0 Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 59/96 FACULTY OF INFORMATICS Masaryk University Multiple Instances of a Process Newgaine < Game I Block Blockgame SIGNAL Game aver Game overs ck JGameoveí J R4 JBumpJ [Vlewgame J Bump, Game ove rack / \ Monitor (1,1) Game(0,) w v_ J V_ / Probe, Result, Endgame R2 R3 Gameid, Win, Lost, Score Deamonserver.in De am on server, out Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. 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 2020 This presentation is not a self-contained study material. It is 61/96 FACULTY OF INFORMATICS Masaryk University SDL - Overview system example_3 (3 In sysle m example Systems ami blocks cttn contain hiocks ánti/orprocesses. Processes contain j behaviour £stdcannot f contain hiocks. - procedure pr 1 (1) Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 63/96 FACULTY OF INFORMATICS I 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 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 64/96 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 2020 This presentation is not a self-contained study material. It is 65/96 FACULTY OF INFORMATICS Masaryk University Petri Nets Petri Nets J Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 66/96 FACULTY OF INFORMATICS Masaryk University Petri Nets C.A. Petri: Kommunikation mit automaten, 1962 Basic components: ■ places places with tokens inside ■ transitions ■ tokens ■ arcs transition Marking = configuration = distribution of tokens = vector of token #s in places A transition can be fired if there is a token in each of its input places. J Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 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 0 output places Tokens from input places are removed and new tokens are added into Vojtěch Řehák . Specifics &y teWfoi^.^SnQ^ self-contained study material. It is 67/96 FACULTY OF INFORMATICS Masaryk University Demonstration Example #1 YellowToRed GreenToYellow RedToRedyellow RedyellowTüGreen Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 68/96 FACULTY OF INFORMATICS Masaryk University Demonstration Example #1 YellowToRed GreenToYellow RedToRedyellow RedyellüwTüGreen What is wrong in this example? j Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 68/96 FACULTY OF INFORMATICS Masaryk University Demonstration Example #2 Better and a bit more complicated example. red_yellow 69/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Sequential execution Iteration Alternative Parallel execution Vojtcrch Reflak • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 70/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Semaphore Rende-vous Vojtěch WarKvBSpecification and Vei Spring 2020 This tudy material. It is 71/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Alternation Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Alternation Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Alternation Deadlock Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 73/96 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 2020 This presentation is not a self-contained study material. It is 74/96 FACULTY OF INFORMATICS I Masaryk University Transition-Place Petri Nets An arbitrary number of tokens in each place. producer consumer notification channel l^dilA0e>IWG0^ G ha 13 ^[contained study material. It is 75/96 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 76/96 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 76/96 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 76/96 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 76/96 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 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 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 ti pi 1/ P2 r i(o)rificat| Voj^Bh ReháJ&_>5pecifiHion arYd^yerificat^ • Spring 2020 This presentation is not a s^f-copfained study material. It is 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- Vojtěch Řehák • Specification and is not a self-contained study material. It is 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._J Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 80/96 FACULTY OF INFORMATICS Masaryk University Coloured Petri Net Example - (n.p) JVtortTManů^initValue = 1 (Int) n (n.p) + Transmit Packet (lni) initVaíue = 1 if n=k h (n-P) [inl,Data] J then p else null if n=k then k+i else k RfiClflV? Packet 7 if n=k the k+1 else k n Transmit VoitěcHi Řehák1» Specification and Ve^jjfijóatíon • Spring 202t):=:This presentation anMotfa self-contained study material. It is n 81/96 FACULTY OF INFORMATICS Masaryk University Hierarchical Petri Nets User Request Abstract Workflow Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 82/96 FACULTY OF INFORMATICS 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, w - - udQterministic, or aeneral distributigns) ,„ . M M . . Vojtech RehaR • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 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 I http://cs.au.dk/cpnets/industrial-use/ I Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 84/96 FACULTY OF INFORMATICS Masaryk University Oueueing theory Oueueing theory J Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 86/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?" Our motivation example: 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 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. • • • 87/96 FACULTY OF INFORMATICS I 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 2020 This presentation is not a self-contained study material. It is 88/96 FACULTY OF INFORMATICS Masaryk University Oueueing Networks Requests RAIDO Disk 1 Disk 2 Disk 3 JoinO Reply Apache - MaxClients = 100 LoadBalancer Web Server 1 Jr Web Server 2 ■ open and closed networks ■ system dependences ■ traffic intensity ■ occupancy (on different servers), bottleneck detection,... Vojt^h^gjja^ ^tj>fffTc^1'*tt)a"StYJC!c^1^^! C SP^13"F5 Presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 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 Po = 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 7 = 1/(m-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 2020 This presentation is not a self-contained study material. It is 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 2020 This presentation is not a self-contained study material. It is 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 fi 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 {^dAMSCL QMhcSfffliadf^ study material. It 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 2020 This presentation is not a self-contained study material. It is 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 ■ http://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 2020 This presentation is not a self-contained study material. It is 94/96 FACULTY OF INFORMATICS Masaryk University Relevant Lectures IV113 Úvod do vaLidace a verifikace (Barnat) 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) Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 95/96 FACULTY OF INFORMATICS Masaryk University References ■ ITU-T recommendation Z.120: Message Sequence Charts (MSC). 2011. ■ ITU-T recommendation Z.100: Specification Description Language (SDL). 2016. ■ 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. 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 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 a L. Fundamentals of Queuing Theory. Wiley, 2008. Vojtěch Řehák • Specification and Verification • Spring 2020 This presentation is not a self-contained study material. It is 96/96