Archiv závěrečné práce Petr Slovák FI B-IN BcIN

Mgr. Petr Slovák

Race Conditions in Message Sequence Charts

Race Conditions in Message Sequence Charts

Abstract: Race condition problem is known to be decidable for Message Sequence Charts (MSC) but it becomes undecidable for High-level MSC. This thesis introduces a modification of the race condition problem, so called trace race condition problem, that remains decidable even for High-level MSC (with coregions). In this thesis, we discuss differences between the race condition and the trace race condition problem and we argue that our concept is useful in model based design. We also propose an algorithm solving the trace race condition problem as well as show the problem itself to be NP-complete for HMSC with coregions. …víceméně

Message Sequence Charts, High-level Message Sequence Charts, race conditions, trace race conditions

Zadání: Moderní aplikace pro mobilní sítě jsou často vytvářeny na bázi protokolu SIP (Session Initiation Protocol), který poskytuje příslušná komunikační a signalizační primitiva. Velkým problémem je zaručení robustnosti a konzistence nových aplikací s již existujícími aplikacemi. Při návrhu nových aplikací se používají různé modelovací jazyky, které slouží jednak k přehlednému a systematickému zápisu, ale hlavně umožňují do vývojového cyklu aplikací zapojit automatizované metody hledání chyb a ověřování korektnosti (např. problém race condition a non-local choice).

Spolu s průmyslovými partnery jsme jako vhodný formalismus vybrali Message Sequence Charts (MSC) a zvláště pak rozšířenou variantou High-level Message Sequence Charts (HMSC). Oba tyto formalizmy byly zavedeny v ITU specifikaci Z.120.

Úkolem studenta je zaměřit se zvláště na problém detekce race conditions, prozkoumat možnosti této automatické verifikace nad návrhy v MSC a HMSC, shrnout známé teoretické výsledky, posoudit jejich relevanci a navrhnout případná vylepšení vhodná pro praktické použití při návrhu reálných síťových protokolů.

Dílčí úkoly a požadavky:

• Nastudujte ITU-T standard Z.120 popisující Message Sequence Charts (MSC); • Prozkoumejte publikované možnosti automatického ověřování race condition. • Posuďte relevanci nalezených výsledků a případně navrhněte vylepšení vhodná pro praktické využití při návrhu reálných síťových protokolů.

Literatura a odkazy:

[1] Message Sequence Charts (MSC), ITU-T recommendation Z.120 (04/2004)

[2] SCStudio, http://sourceforge.net/projects/scstudio …víceméně

Jazyk práce: angličtina