Verifying Temporal Properties of Use-Cases in Natural Language

0369573 - ÚI 2014 DE eng C - Konferenční příspěvek (zahraniční konf.)
Šimko, V. - Hauzar, D. - Bureš, Tomáš - Hnětynka, P. - Plášil, František
Verifying Temporal Properties of Use-Cases in Natural Language.
Formal Aspects of Component Software. Berlin: Springer, 2012 - (Arbab, F.; Ölveczky, P.), s. 350-367. Lecture Notes in Computer Science, 7253. ISBN 978-3-642-35742-8. ISSN 0302-9743.
[FACS 2011. International Symposium on Formal Aspects of Component Software /8./. Oslo (FI), 14.09.2011-16.09.2011]
Grant ostatní: GA AV ČR(CZ) GAP103/11/1489
Klíčová slova: use-cases * behavior modeling * verification * natural language * label transition system * model-checking * requirements engineering * temporal logic
Kód oboru RIV: JC - Počítačový hardware a software

This paper presents a semi-automated method that helps iteratively write use-cases in natural language and verify consistency of behavior encoded within them. In particular, this is beneficial when the use-cases are created simultaneously by multiple developers. The proposed method allows verifying the consistency of textual use-case specification by employing annotations in usecase steps that are transformed into temporal logic formulae and verified within a formal behavior model. A supporting tool for plain English use-case analysis is currently being enhanced by integrating the verification algorithm proposed in the paper.
Trvalý link: http://hdl.handle.net/11104/0203603