Název: Formální vertifikace textových use casů
Překlad názvu: Verification of Textual Use-Cases
Autoři: Vinárek, Jiří ; Šimko, Viliam (vedoucí práce) ; Hauzar, David (oponent)
Typ dokumentu: Diplomové práce
Rok: 2013
Jazyk: eng
Abstrakt: [eng] [cze]
The aim of this thesis is to create a tool for formal verification of systems specified using textual use- cases. The tool should allow for automated verification of temporal invariants specified in temporal logic (CTL and LTL formulae). The textual specification is transformed to a formal model that is verified using the NuSMV symbolic model-checker. Potential errors are shown to the user in the form of an HTML report. Using this feedback, the user is able to iteratively develop valid textual use-case specifications. The tool's architecture should be focused on reusability of its components and extensibility. Powered by TCPDF (www.tcpdf.org) Cílem práce je poskytnout nástroj pro formální verifikaci systému, který je popsán pomocí textových případů užití (textual use cases). Nástroj umožňuje automatické ověření invariantů vyjádřených pomocí formulí temporální logiky (CTL nebo LTL). Textová specifikace je transformována na formální model, který je pomocí NuSMV symbolického model-checkeru verifikován a případné chyby jsou zobrazeny uživateli. Výstupem je přehledný HTML report, který pomocí zpětné vazby umožňuje uživateli iterativní vývoj validních textových use-case specifikací. Architektura nástroje je volena s ohledem na znovupoužitelnost jednotlivých modulů a budoucí možné rozšíření. Powered by TCPDF (www.tcpdf.org)
Klíčová slova: Formal Methods; NuSMV; Requirements; Specification; Verification; Formal Methods; NuSMV; Requirements; Specification; Verification

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/52119

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-321436


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Diplomové práce