30 - Formální metody v počítačových sítích: modelování protokolů pomocí konečných automatů a temporálních logik.
pondělí 21. května 2018
17:24
Protokolové inženýrství
Validace: vyhodnocení protokolu z hlediska realizace služeb 
Verifikace: ověření správnosti specifikace
jednoznačnost 
bezpečnost 
Konverze protokolů: pro propojování sítí, vývoj protokolů 
Výkonnostní analýza: zkoumání vlivu parametrů na celkovou výkonnost
Testování: experimentální ověřování, zda implementace odpovídá specifikaci
Vývoj protokolů:
Analytický přístup - předběžné navržený protokol je verifikován a validován, což vede na změny v návrhu resp. opakovaný návrh (iterace) 
Syntetický přístup - částečně specifikovaný protokol je konstruován podle požadavků korektnosti a validity
Formální prostředky
orientace na model
konečné automaty
formalizované sítě, petriho sítě
programovací jazyky CCITT(Chill), prolog, pascal, ada
metody abstraktních modelů, relační notace
přechodové
algebry procesů
stopy (TRACE)
atributové gramatiky
orientace na vlastnosti
algebraické metody
axiomatické metody, teorie množin, predikátová logika = metody abstraktních modelů, relační notace
From <[link]> 
Konečné automaty
[link]
Příklad:
KA + Temp. logika pro 3 way handshake
Notes 
Otazka (okruh): 104. Protokolové inženýrství a formální specifikace protokolů (konečné automaty, gramatiky, stopy, relace, temporální logika).
Kdo me primarne zkousel: Švéda Miroslav, prof. Ing., CSc.
Co jsem k tomu rekl(a)/na co se ptali/co mne vytkli: Túto otázku som sa snažil pochopiť ale nešlo to (nebol som skoro vôbec naučený a to som sieťar a vedel som všetko zo sietí od A po Z). Dostal som zo seba základné veci známe z návrhu protokolov a ako fungujú ale to vedieť moc nechcel. Celú dobu sa zo mňa snažil vypáčiť prečo zapisujeme protokoly formálne. Jediné, na čo som sa zmohol bola validace, verifikace a to pomocou matematických dôkazov (chcel dalsie veci). Myslel som, že letím s F ale Švéda je borec. Známka C
From <[link]> 