BABICA, Jindřich, Vojtěch ŘEHÁK, Petr SLOVÁK, Pavel TROUBIL a Martin ZAVADIL. Formalisms and Tools for Design and Specification of Network Protocols. Online. Brno: FI MU, 2007. FIMU-RS-2007-02. [citováno 2024-04-24]
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Formalisms and Tools for Design and Specification of Network Protocols
Název česky Formalizmy a nástroje pro navrh a specifikaci sitovych protokolu
Autoři BABICA, Jindřich (203 Česká republika), Vojtěch ŘEHÁK (203 Česká republika, garant, domácí), Petr SLOVÁK (203 Česká republika, domácí), Pavel TROUBIL (203 Česká republika) a Martin ZAVADIL (203 Česká republika)
Vydání Brno, FIMU-RS-2007-02, 2007.
Nakladatel FI MU
Další údaje
Originální jazyk angličtina
Typ výsledku Audiovizuální tvorba
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Česká republika
Utajení není předmětem státního či obchodního tajemství
WWW URL
Kód RIV RIV/00216224:14330/07:00019613
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky Network protocol description; Message Sequence Charts; realizability; race conditions; formal verification
Štítky formal verification, Message Sequence Charts, Network protocol description, race conditions, realizability
Příznaky Mezinárodní význam
Změnil Změnil: RNDr. Pavel Troubil, Ph.D., učo 139885. Změněno: 13. 6. 2013 12:25.
Anotace
Message Sequence Charts (MSC) are a useful formalism for formalization of network protocols early in their design phase. In this paper, we introduce the basics of MSC language and describe some of the possibilities for automatic location of "problematic" parts in the design. Focus is then given to different modifications of MSC design (FIFO behavior, bounded channels, etc. ) as well as formal checking of more complex design properties (MSC membership, realizability). Next, an introduction of Specification and Description Language (SDL) is presented. Possibilities of automatic synthesis of system design in MSC to an SDL model and it`s correctness verification are mentioned.
Anotace česky
Message Sequence Charts (MSC) jsou užitečným formalizmem pro popis síťových protokolu v ranné fázi jejich návrhu. V tomto přízpěvku uvádíme základy jazyka MSC a popisujeme možnosti jeho využití při modelování problematických části návrhu. Dále se zaměřujeme na možné modifikace MSC popisu (FIFO chování, omezení datových kanálů, atd.) stejně jako na možnosti automatického ověření správnosti (MSC membership, realizavatelnost). Stručně též zavádíme Specification and Description Language (SDL).
Návaznosti
GD102/05/H050, projekt VaVNázev: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 24. 4. 2024 02:34