Original title: Formální vertifikace textových use casů
Translated title: Verification of Textual Use-Cases
Authors: Vinárek, Jiří ; Šimko, Viliam (advisor) ; Hauzar, David (referee)
Document type: Master’s theses
Year: 2013
Language: eng
Abstract: [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)
Keywords: Formal Methods; NuSMV; Requirements; Specification; Verification; Formal Methods; NuSMV; Requirements; Specification; Verification

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/52119

Permalink: http://www.nusl.cz/ntk/nusl-321436


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Master’s theses