LTS semantics for use case models

Formalization is a necessary precondition for the specification of precise and unambiguous use case models, which serve as reference points for the design and implementation of software systems. In this paper, we define a formal semantics for use case We build on an abstract syntax definition formalizing the sequencing of use case steps. As a semantic domain we have chosen Labeled Transition Systems (LTSs), which, we believe, intuitively capture the behavioral aspects of the use case model. The mapping into LTSs is defined over the various structural elements of the use case model. The proposed formal semantics allows for various semantic checks such as detection of livelocks and validation of model refinement, an important property in an iterative software development lifecycle. We also introduce our tool “Use Case Model Analyzer”. Categories and Subject Descriptors D.2.1 [Software Engineering]: Requirements/Specifications – languages, methodologies, tools. Keywords Requirement...

• Type: Conference
• Year: 2009
• Where: SAC
• Authors: Daniel Sinnig, Patrice Chalin, Ferhat Khendek
• Keywords: Applied Computing, Case Model, Formal Semantics, SAC 2009, Use Cases