Název: Z textové specifikace k formální verifikaci
Překlad názvu: From textual specification to formal verification
Autoři: Šimko, Viliam ; Hnětynka, Petr (vedoucí práce) ; Gruhn, Volker (oponent) ; Steinberger, Josef (oponent)
Typ dokumentu: Disertační práce
Rok: 2013
Jazyk: eng
Abstrakt: [eng] [cze]
Textual use-cases have been traditionally used at the design stage of the software development process to describe software functionality from the user's perspective. Because use-cases typically rely on natural language, they cannot be directly subject to formal verification. Another important artefact is the domain model, a high-level overview of the most important concepts in the problem space. A domain model is usually not constructed en bloc, yet it undergoes refinement starting from the first prototype elicited from text. This thesis covers two closely related topics - formal verification of use-cases and elicitation of a domain model from text. The former is a method (called FOAM) that features simple user-definable annotations inserted into a use-case to make it suitable for verification. A model-checking tool is employed to verify temporal invariants associated with the annotations while still keeping the use-cases understandable for non-experts. The latter is a method (titled Prediction Framework) that features an in-depth linguistic analysis of text and a sequence of statistical classifiers (log-linear Maximum Entropy models) to predict the domain model. Běžný způsob popisu funkčních požadavků při vývoji softwaru je tvorba textových případů použití (use-cases). Jejich úlohou v úvodních fázích projektu je zachytit formou přirozeného jazyka způsob fungování systému z pohledu koncového uživatele. Protože jde o text psaný v přirozeném jazyce, není možné správnost textových případů použití přímo formálně ověřovat. Obdobně významným artefaktem při vývoji software je doménový model. Jde o popis nejdůležitějších konceptů a vztahů, které jsou pro vyvíjenou aplikaci důležité. Tvorba doménového modelu běžně probíhá iterativně od prvního prototypu z textu až po výsledný formální model. Tato práce se zabývá dvěma souvisejícími tématy - formální ověřování případů použití a odvozování doménového modelu z textu. První část je věnovaná metodě FOAM, která umožňuje pomocí jednoduchých anotací vložených do textu případů použití formálně ověřovat jejich správnost (model-checking). Anotace umožňují zachytit větvení kroků v případech použití a uživatel má možnost vyjádřit časové závislosti mezi různými částmi specifikace, zároveň je však zachovaná srozumitelnost původního textu. Druhá část práce popisuje tzv. Prediction Framework, který pomocí lingvistické analýzy textu a statistických klasifikátorů (log-linear Maximum Entropy models) umožňuje predikování doménového model z textu.
Klíčová slova: Formální metody; Modelování; Požadavky; Verifikace; Formal Methods; Modeling; Requirements; 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/52925

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


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 > Disertační práce