Formalisms and Tools for Design and Specification of Network Protocols

BABICA, Jindřich, Vojtěch ŘEHÁK, Petr SLOVÁK, Pavel TROUBIL and Martin ZAVADIL. Formalisms and Tools for Design and Specification of Network Protocols. Brno: FI MU, 2007. FIMU-RS-2007-02.

Basic information

Original name

Formalisms and Tools for Design and Specification of Network Protocols

Name in Czech

Formalizmy a nástroje pro navrh a specifikaci sitovych protokolu

Authors

BABICA, Jindřich (203 Czech Republic), Vojtěch ŘEHÁK (203 Czech Republic, guarantor, belonging to the institution), Petr SLOVÁK (203 Czech Republic, belonging to the institution), Pavel TROUBIL (203 Czech Republic) and Martin ZAVADIL (203 Czech Republic)

Edition

Brno, FIMU-RS-2007-02, 2007

Publisher

FI MU

---

Other information

Language

English

Type of outcome

Audiovizuální tvorba

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

References:

URL

RIV identification code

RIV/00216224:14330/07:00019613

Organization unit

Faculty of Informatics

Keywords in English

Network protocol description; Message Sequence Charts; realizability; race conditions; formal verification

Tags

formal verification, Message Sequence Charts, Network protocol description, race conditions, realizability

Tags

International impact

---

Abstract

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.

In Czech

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).

---

Links

GD102/05/H050, research and development project	Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science