Other formats:
BibTeX
LaTeX
RIS
@misc{759822,
author = {Babica, Jindřich and Řehák, Vojtěch and Slovák, Petr and Troubil, Pavel and Zavadil, Martin},
address = {Brno},
keywords = {Network protocol description; Message Sequence Charts; realizability; race conditions; formal verification},
language = {eng},
location = {Brno},
publisher = {FI MU},
title = {Formalisms and Tools for Design and Specification of Network Protocols},
url = {http://www.fi.muni.cz/reports/2007/abstract/FIMU-RS-2007-02.shtml},
year = {2007}
}
TY - GEN
ID - 759822
AU - Babica, Jindřich - Řehák, Vojtěch - Slovák, Petr - Troubil, Pavel - Zavadil, Martin
PY - 2007
TI - Formalisms and Tools for Design and Specification of Network Protocols
VL - FIMU-RS-2007-02
PB - FI MU
CY - Brno
KW - Network protocol description
KW - Message Sequence Charts
KW - realizability
KW - race conditions
KW - formal verification
UR - http://www.fi.muni.cz/reports/2007/abstract/FIMU-RS-2007-02.shtml
L2 - http://www.fi.muni.cz/reports/2007/abstract/FIMU-RS-2007-02.shtml
N2 - 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.
ER -
BABICA, Jindřich, Vojtěch ŘEHÁK, Petr SLOVÁK, Pavel TROUBIL and Martin ZAVADIL. \textit{Formalisms and Tools for Design and Specification of Network Protocols}. Brno: FI MU, 2007. FIMU-RS-2007-02.
|
