A 2007

Formalisms and Tools for Design and Specification of Network Protocols

BABICA, Jindřich; Vojtěch ŘEHÁK; Petr SLOVÁK; Pavel TROUBIL; Martin ZAVADIL et. al.

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

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í

Odkazy

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

Příznaky

Mezinárodní význam
Změněno: 13. 6. 2013 12:25, RNDr. Pavel Troubil, Ph.D.

Anotace

ORIG CZ

V originále

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.

Č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 VaV
Ná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ěr
Ná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 VaV
Ná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 VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky