Formal Verification of Annotated Textual Use-Cases

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F15%3A10281519" target="_blank" >RIV/00216208:11320/15:10281519 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/67985807:_____/15:00446568

Výsledek na webu

<a href="http://comjnl.oxfordjournals.org/content/early/2014/09/08/comjnl.bxu068.full.pdf+html" target="_blank" >http://comjnl.oxfordjournals.org/content/early/2014/09/08/comjnl.bxu068.full.pdf+html</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1093/comjnl/bxu068" target="_blank" >10.1093/comjnl/bxu068</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Formal Verification of Annotated Textual Use-Cases

Popis výsledku v původním jazyce

Textual use-cases have been traditionally used in the initial stages of the software development process to describe software functionality from the user's perspective. Their advantage is that they can be easily understood by stakeholders and domain experts. However, since use-cases typically rely on natural language, they cannot be directly subject to a formal verification. In this article, we present a method (called Formal Verification of Annotated Use-Case Models, FOAM) for formal verification of use-cases. This method features simple user-definable annotations, which are inserted into a use-case to make its semantics more suitable for verification. Subsequently, a model-checking tool is employed to verify temporal invariants associated with the annotations. This way, FOAM allows harnessing the benefits of model checking while still keeping the use-cases understandable for non-experts.

Název v anglickém jazyce

Formal Verification of Annotated Textual Use-Cases

Popis výsledku anglicky

Textual use-cases have been traditionally used in the initial stages of the software development process to describe software functionality from the user's perspective. Their advantage is that they can be easily understood by stakeholders and domain experts. However, since use-cases typically rely on natural language, they cannot be directly subject to a formal verification. In this article, we present a method (called Formal Verification of Annotated Use-Case Models, FOAM) for formal verification of use-cases. This method features simple user-definable annotations, which are inserted into a use-case to make its semantics more suitable for verification. Subsequently, a model-checking tool is employed to verify temporal invariants associated with the annotations. This way, FOAM allows harnessing the benefits of model checking while still keeping the use-cases understandable for non-experts.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP103%2F11%2F1489" target="_blank" >GAP103/11/1489: Metody pro tvorbu a ověřování komponentových systémů ze specifikací v přirozeném jazyce</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Computer Journal

ISSN

0010-4620

e-ISSN

—

Svazek periodika

58

Číslo periodika v rámci svazku

7

Stát vydavatele periodika

GB - Spojené království Velké Británie a Severního Irska

Počet stran výsledku

35

Strana od-do

1495-1529

Kód UT WoS článku

000359141100001

EID výsledku v databázi Scopus

2-s2.0-84937053805