FACULTY OF INFORMATICS Masaryk University PA160: Net-Centric Computing II. Specification and Verification of Network Protocols Vojtěch Řehák Spring 2019 Vojtěch Řehák • Specification and Verification • Spring 2019 1/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage Theory Vojtěch Řehák • Specification and Verification • Spring 2019 2/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage Vojtěch Řehák • Specification and Verification • Spring 2019 2/96 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage T Vojtěch Řehák • Specification and Verification • Spring 2019 FACULTY OF INFORMATICS Masaryk University Theory Definition and Usage Vojtěch Řehák • Specification and Verification • Spring 2019 FACULTY OF INFORMATICS Masaryk University Theoretical Results as Tools for Users Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 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 2019 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 2019 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 2019 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 2019 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 2019 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 2019 6/96 FACULTY OF INFORMATICS I 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 2019 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 2019 8/96 FACULTY OF INFORMATICS Masaryk University Distributed Systems World is distributed Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 FACULTY OF INFORMATICS Masaryk University Distributed vs. Local SDL Specification Description Language MSC Message Sequence Chart ITU-T Z.100 Input Output > (Telephone \ on-hook } \ Calleigoes / offJiook jL Caller gete O ( DtaJ tone ITU-T Z.120 C>1 hCltsMEMl |ir',r]|| t|i,| n.| lI K--.||.|rlll ÍI lI Rirri|ibnil lirM liLtlirl 111 rl 1 " ii hlcmjAlAitqimi Graphical specific ail on HÍTSDA1 ^.4-rtiidipn i- ^ttB'.ifl lul tllMH fi\i UM V in ■■■ --■■ i- i modeLs of components communication model Vojtěch Řehák • Specification and Verification • Spring 2019 10 / 96 FACULTY OF INFORMATICS Masaryk University Message Sequence Chart (MSC) Message Sequence Chart (MSC) Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 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 2019 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 2019 14/96 FACULTY OF INFORMATICS Masaryk University Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2019 15/96 FACULTY OF INFORMATICS I Masaryk University Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2019 15/96 FACULTY OF INFORMATICS I Masaryk University Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2019 15/96 FACULTY OF INFORMATICS I Masaryk University Message Sequence Chart (MSC) - semantics Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2019 15/96 FACULTY OF INFORMATICS I Masaryk University MSC - Visual Order Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2019 16/96 FACULTY OF INFORMATICS I Masaryk University MSC - Visual Order - Hasse Diagram Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2019 17/96 FACULTY OF INFORMATICS Masaryk University MSC Properties What is an unwanted behaviour/property? Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 19 / 96 J 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 2019 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 2019 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 2019 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 2019 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 realizable in an environment with P2P channels but unrealizable in case of one global channel Vojtěch Řehák • Specification and Verification • Spring 2019 21 / 96 FACULTY OF INFORMATICS Masaryk University Race Condition Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2019 22/96 FACULTY OF INFORMATICS Masaryk University Race Condition Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2019 22/96 FACULTY OF INFORMATICS Masaryk University Race Condition Peter Jane Paul Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 FACULTY OF INFORMATICS I 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 2019 23/96 FACULTY OF INFORMATICS Masaryk University Solution #1 - Coregion Construction Let us demonstrate that some events are not ordered. Peter Jane Paul Ma Hyme! Yes. Events in a coregion are not ordered; except for the event related by general ordering. Vojtěch Řehák • Specification and Verification • Spring 2019 23/96 FACULTY OF INFORMATICS Masaryk University Solution #2 - List/set of all possibilities Vojtěch Řehák • Specification and Verification • Spring 2019 24/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) Vojtěch Řehák • Specification and Verification • Spring 2019 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 msc ACsystemOverview connection point HMSC start Idle ^4oop User accepted < Door unlocked Unlocked reset User rejected msc reference restrictive condition Unlocked timeout Unlocked unclosed alternative Vojtěch Řehák • Specification and Verification • Spring 2019 26/96 FACULTY OF INFORMATICS I Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák • Specification and Verification • Spring 2019 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 X7 Trace example: i . i i , i i . i Vojtěch Řehák • Specification and Verification • Spring 2019 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 □ l , l c Trace example: Vojtěch Řehák • Specification and Verification • Spring 2019 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák • Specification and Verification • Spring 2019 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 these events are not ordered! Vojtěch Řehák • Specification and Verification • Spring 2019 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 1 HI Trace example: Vojtěch Řehák • Specification and Verification • Spring 2019 27/96 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák • Specification and Verification • Spring 2019 FACULTY OF INFORMATICS Masaryk University High-Level MSC (HMSC) - ITU-T Z.120 Vojtěch Řehák • Specification and Verification • Spring 2019 27/96 FACULTY OF INFORMATICS Masaryk University Deadlock Property 1 r A B V J L ) Vojtěch Řehák • Specification and Verification • Spring 2019 28/96 FACULTY OF INFORMATICS Masaryk University Livelock Property £ £ B Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 ^ Input BMSC bMSC01 1 f bMSC02 J Input HMSC Instance A Instance B _ _ p bMSCOl Instance A Instance B q ĎMSC02 Vojtěch Řehák • Specification and Verification • Spring 2019 30/96 FACULTY OF INFORMATICS Masaryk University Inline Expressions System 1 i ~i System2 i ~i System3 i ~i Vojtěch Řehák • Specification and Verification • Spring 2019 31/96 FACULTY OF INFORMATICS Masaryk University Inline Expressions System 1 System2 System3 ■ "i i , ~i i , ~i altj ^----^top_____ ^--£22iSüe I I I I I —I Other inline expression types: opt, loop(/77, n), exc, seq, par. Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 32/96 FACULTY OF INFORMATICS Masaryk University Non-local Choice System 1 i "i alt System2 i "i Int System3 System3 does not know which alternative has been chosen. j Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 32/96 FACULTY OF INFORMATICS Masaryk University Non-local Choice System 1 System2 System3 i "i i ~i i ~i altj I I I I I —I System3 does not know which alternative has been chosen. Vojtěch Řehák • Specification and Verification • Spring 2019 32 / 96 FACULTY OF INFORMATICS I 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 2019 33/96 FACULTY OF INFORMATICS 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 2019 33/96 FACULTY OF INFORMATICS I 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 2019 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 2019 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 2019 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 r 1 r A v r m2 m2 m2 m2 ► ► Buffer of size 2 suffices to avoid deadlock. Or one buffer for each message Label (type). Vojtěch Řehák • Specification and Verification • Spring 2019 34/96 FACULTY OF INFORMATICS Masaryk University Race Condition - Solution #3 - Time Constraints Application server Resp1 onse Message er Response Response Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 35/96 FACULTY OF INFORMATICS Masaryk University Time Consistency Are the given time conditions consistent? Client A Proxy Server Vojtěch Řehák • Specification and Verification • Spring 2019 36/96 FACULTY OF INFORMATICS Masaryk University Time Tightening Some time conditions can be tightened, Client A Proxy A" HTTP st HTTP HTTP HTTP Vojtěch Řehák • Specification and Verification • Spring 2019 FACULTY OF INFORMATICS Masaryk University Time Tightening Some time conditions can be tightened. Client A Proxy Server Vojtěch Řehák • Specification and Verification • Spring 2019 37/96 FACULTY OF INFORMATICS Masaryk University Timers Initiator Responder ICONreq ICON tX- altj tX-► LATECONF ICONF ICONF tY 1 A OKCONF Vojtěch Řehák • Specification and Verification • Spring 2019 38/96 FACULTY OF INFORMATICS Masaryk University MSC - Summary Basic MSC ■ instances ■ messages ■ send events ■ receive events ■ conditions ■ coregions ■ general ordering ■ inline expressions ■ time constraints ■ timers High-level MSC (HMSC) ■ start node ■ end node ■ reference nodes ■ connection points ■ Lines ■ conditions ■ time constraints Vojtěch Řehák • Specification and Verification • Spring 2019 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 ■ Tighten Time Vojtěch Řehák • Specification and Verification • Spring 2019 40 / 96 FACULTY OF INFORMATICS I Masaryk University MSC - Goals What MSC is good for? Both human and computer readable formaLizm fo ■ 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 2019 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 2019 41/96 FACULTY OF INFORMATICS I 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 ■ checkers for all the mentioned properties Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 43/96 FACULTY OF INFORMATICS Masaryk University Distributed vs. Local SDL Specification Description Language MSC Message Sequence Chart ITU-T Z.100 Input Output zz > (Telephone \ on-hook } \ Calleigoes / off-hook jL Caller gete > o ( DiaJ tone j J 1 ITU-T Z.120 C>1 hCltsMEMl |ir',r]|| t|i,| n.| lI K"l|'lrlll ÍI lI Mfii|iLnil lirM liLtlirl 111 rl 1 " ii hlcmjATiUtqimi Graph leal specific ail on i- Achim» Munmt pit 0X1 V in ■■■ --■■ i- i models of components communication model Vojtěch Řehák • Specification and Verification • Spring 2019 44/96 FACULTY OF INFORMATICS Masaryk University Specification Description Language (SDL) Specification Description Language (SDL) J Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 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 2019 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 2019 48/96 FACULTY OF INFORMATICS Masaryk University SDL/GR - Process process type diagram. variables process type Controller 1(1] del cur panel Pld ; r current panel whose Code will be validated / del cid, PIN integer; /* temporary variables for the data attributes of 'Code' 7 start Idle state input Validation Xode(dd,PIN^ "V* fi orr Panel 7 OK /* from Central 7 cur_panel SENDER _task OK TO cur_paneL Code(cid,PINÍ I TG CentralUnit next st ate unlockDoor Validatio if I Idle unlockDoor procedure NOK /* from Central 7 NOK TO cur_panel> procedure call output 1 Idle Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 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 2019 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 Access Point 7 display, /* Display TO ENV 7 keys; /*ENV TO Keyboard 7 SIGNAL Code (integer, integer);/'AccessPoint 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 [(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 2019 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 2019 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 2019 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 2019 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 2019 57/96 FACULTY OF INFORMATICS Masaryk University Timer Construction TIMER door timeout set(qj); Vojtěch Řehák • Specification and Verification • Spring 2019 source: TIMe Electronic Textbook v4.0 58/96 FACULTY OF INFORMATICS Masaryk University Multiple Instances of a Block system AccessGontrol 1(1) CE Access Point [(DutpH KlnpH e AP(100): C Access Point d I [(validity)] [Code] GentralUnit [isOpenJsClosed] [lock,unlock] Vojtěch Řehák • Specification and Verification • Spring 2019 source: TIMe Electronic Textbook v4.0 59/96 FACULTY OF INFORMATICS Masaryk University Multiple Instances of a Process N ewgame Game Í Block Blockgame SIGNAL Game over (P; Gameoverack jöairieover J R4 JEumpj Monitor(l,l]) [n ewgame J RJ Bump, Gameoverack Game(0,) Piobe, Result, Endgame R2 J R3 Gameid, Win, Lost, Score Deamonserver.ki D e am on s erver. out Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 61/96 FACULTY OF INFORMATICS Masaryk University SDL - Overview system example system example Systems ami blacks can contain óioeks anti/orprocesses. + Pmcesses contain heha\ 'ioarand cannot contain hhxrks* procedure pr 1 (1) CT7D I ^) Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 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 2019 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 2019 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 2019 FACULTY OF INFORMATICS Masaryk University Petri Nets Petri Nets J Vojtěch Řehák • Specification and Verification • Spring 2019 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 Marking = configuration = distribution of tokens = vector of token #s in places 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 2019 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 the output places of the fired transition. Vojtěch Řehák • Specification and Verification • Spring 2019 67/96 FACULTY OF INFORMATICS Masaryk University Demonstration Example #1 YellowToRed GreenToYellow Vojtěch Řehák • Specification and Verification • Spring 2019 68 / 96 FACULTY OF INFORMATICS Masaryk University Demonstration Example #1 YellowToRed GreenToYellow RedToRedyellow RedyellowToGreen What is wrong in this example? J Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 69 / 96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Sequential execution Iteration Alternative Parallel execution Vojtěch Řehák • Specification and Verification • Spring 2019 70/96 FACULTY OF INFORMATICS I Masaryk University Basic Constructions Semaphore Rende-vous Vojtěch Řehák • Specification and Verification • Spring 2019 FACULTY OF INFORMATICS Masaryk University Basic Constructions Vojtěch Řehák • Specification and Verification • Spring 2019 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Vojtěch Řehák • Specification and Verification • Spring 2019 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Vojtěch Řehák • Specification and Verification • Spring 2019 72/96 FACULTY OF INFORMATICS Masaryk University Basic Constructions Critical section Alternation Vojtěch Řehák • Specification and Verification • Spring 2019 72/96 FACULTY OF INFORMATICS Masaryk University Critical section Alternation Vojtěch Řehák • Specification and Verification • Spring 2019 72/96 FACULTY OF INFORMATICS Masaryk University Critical section Alternation Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 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 2019 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity Vojtěch Řehák • Specification and Verification • Spring 2019 76/96 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity Vojtěch Řehák • Specification and Verification • Spring 2019 76/96 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity Vojtěch Řehák • Specification and Verification • Spring 2019 FACULTY OF INFORMATICS Masaryk University Additional Constructs - Arc Multiplicity 3 Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 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 2019 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 2019 80/96 FACULTY OF INFORMATICS Masaryk University Coloured Petri Net Example Vojtěch Řehák • Specification and Verification • Spring 2019 81/96 FACULTY OF INFORMATICS Masaryk University Hierarchical Petri Nets Vojtěch Řehák • Specification and Verification • Spring 2019 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, deterministic, or general distributions) Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 84/96 FACULTY OF INFORMATICS Masaryk University Oueueing theory Oueueing theory J Vojtěch Řehák • Specification and Verification • Spring 2019 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 2019 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 2019 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 2019 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 2019 88 / 96 FACULTY OF INFORMATICS Masaryk University Oueueing Networks s- I Requests RAIDO Disk 1 Disk 2 Disk 3 JoinO Reply Apache - MaxClients = 100 LoadBalancer Web Server 1 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 2019 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 2019 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 2019 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 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 2019 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 2019 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 2019 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 2019 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 2019 94/96 FACULTY OF INFORMATICS Masaryk University Relevant Lectures r IV113 Uvod 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 2019 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). 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 2019 96/96