Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

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 models. 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".

REFERENCES

• 1: Ivar Jacobson, Object-Oriented Software Engineering: A Use Case Driven Approach, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 2004
• 2: Craig Larman, Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and Iterative Development (3rd Edition), Prentice Hall PTR, Upper Saddle River, NJ, 2004
• 3: Merrick, P. and Barrow, P., The Rationale for OO Associations in Use Case Modelling, in Journal of Object Technology, 4(9), pp. 123--142, 2005.
• 4: Alistair Cockburn, Writing Effective Use Cases, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 5: Somé, S., Petri Nets Based Formalization of Textual Use Cases, Tech. Report in SITE, TR2007-11, Uni. of Ottawa, 2007.
• 6: Robert M. Keller, Formal verification of parallel programs, Communications of the ACM, v.19 n.7, p.371-384, July 1976 [doi>10.1145/360248.360251]
• 7: Butler, G., Grogono, P. and Khendek, F., A Z Specification of Use Cases, in Proceedings of APSEC 1998, pp. 94--101, 1998.
• 8: Mike Barnett , Wolfgang Grieskamp , Wolfram Schulte , Nikolai Tillmann , Margus Veanes, Validating Use-Cases with the AsmL Test Tool, Proceedings of the Third International Conference on Quality Software, p.238, November 06-07, 2003
• 9: W. Grieskamp , M. Lepper , W. Schulte , N. Tillmann, Testable Use Cases in the Abstract State Machine Language, Proceedings of the Second Asia-Pacific Conference on Quality Software, p.167, December 10-11, 2001
• 10: Mizouni, R., Salah, A., Kolahi, S. and Dssouli, R., Merging partial system behaviours: composition of use-case automata, in Software, IET, 1(4), pp. 143--160, 2007.
• 11: Nipkow, T., Paulson, L. and Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher Order Logic, Springer, 1998.
• 12: Sinnig, D., Use Case and Task Models: Formal Framework and Integrated Development Methodology, PhD Thesis in Department of Computer Science and Software Engineering, Concordia University, Montreal, 2008.
• 13: A. W. Roscoe , C. A. R. Hoare , Richard Bird, The Theory and Practice of Concurrency, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 14: CADP, Construction and Analysis of Distributed Processes - Software Tools for Designing Reliable Protocols and Systems {Internet}, Available from http://www.inrialpes.fr/vasy/cadp/, Accessed: May 2007, Last Update: 2007.
• 15: Jeff Magee , Jeff Kramer, Concurrency: state models & Java programs, John Wiley & Sons, Inc., New York, NY, 2000
• 16: A. W. Roscoe, Model-checking CSP, A classical mind: essays in honour of C. A. R. Hoare, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 17: Sinnig, D., Chalin, P. and Khendek, F., Consistency between Task Models and Use Cases, in Proc. of DSV-IS, Spain, 2007.
• 18: Daniel Sinnig , Patrice Chalin , Ferhat Khendek, Towards a Common Semantic Foundation for Use Cases and Task Models, Electronic Notes in Theoretical Computer Science (ENTCS), 183, p.73-88, July, 2007 [doi>10.1016/j.entcs.2007.01.062]
• 19: Salinesi, C., Authoring Use Cases, chapter in Scenarios, Stories, Use Cases: Through the Systems Development Life-Cycle. I. Alexander and N. Maiden, John Wiley.
• 20: Keith Thomas Phalp , Jonathan Vincent , Karl Cox, Improving the quality of use case descriptions: empirical assessment of writing guidelines, Software Quality Control, v.15 n.4, p.383-399, December 2007 [doi>10.1007/s11219-007-9023-6]
• 21: Peter Fröhlich , Johannes Link, Automated Test Case Generation from Dynamic Models, Proceedings of the 14th European Conference on Object-Oriented Programming, p.472-492, June 12-16, 2000
• 22: Liwu Li, Translating Use Cases to Sequence Diagrams, Proceedings of the 15th IEEE international conference on Automated software engineering, p.293, September 11-15, 2000
• 23: Avik Sinha , Amit Paradkar , Clay Williams, On Generating EFSM models from Use Cases, Proceedings of the 29th International Conference on Software Engineering Workshops, p.97, May 20-26, 2007 [doi>10.1109/ICSEW.2007.152]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Tools; Methodologies (e.g., object-oriented, structured)

Keywords:
LTSs, requirements, semantics, use cases