Publication at Faculty of Mathematics and Physics |
2012
Abstract
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 use-case steps that are transformed into LTL 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.