Original title:
Z textové specifikace k formální verifikaci
Translated title:
From textual specification to formal verification
Authors:
Šimko, Viliam ; Hnětynka, Petr (advisor) ; Gruhn, Volker (referee) ; Steinberger, Josef (referee) Document type: Doctoral theses
Year:
2013
Language:
eng Abstract:
[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.
Keywords:
Formal Methods; Modeling; Requirements; Verification; Formální metody; Modelování; Požadavky; Verifikace
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/52925