Publikace na Matematicko-fyzikální fakulta |
2012
Abstrakt
The advantage of textual use-cases is that they can be easily understood by stakeholders and domain experts. However, since use-cases typically rely on a natural language, they cannot be directly subject to a formal verification.
In this paper, we present the FOAM method which features simple user-definable annotations, inserted into a use-case to make its semantics more suitable for verification. Subsequently a model-checking tool verifies temporal invariants associated with the annotations.
This way, FOAM allows for harnessing the benefits of model-checking while still keeping the use-cases understandable for non-experts.