Formal Verification of Annotated Textual Use-Cases

Result code in 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>

Alternative codes found

RIV/67985807:_____/15:00446568

Result on the web

<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>

Result language

angličtina

Original language name

Formal Verification of Annotated Textual Use-Cases

Original language description

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.

Czech name

—

Czech description

—

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

<a href="/en/project/GAP103%2F11%2F1489" target="_blank" >GAP103/11/1489: Methods of development and verification of component-based applications using natural language specifications</a><br>

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2015

Confidentiality

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

Name of the periodical

Computer Journal

ISSN

0010-4620

e-ISSN

—

Volume of the periodical

58

Issue of the periodical within the volume

7

Country of publishing house

GB - UNITED KINGDOM

Number of pages

35

Pages from-to

1495-1529

UT code for WoS article

000359141100001

EID of the result in the Scopus database

2-s2.0-84937053805