Composition of use cases using synchronization and model checking

R. Mizouni, A. Salah, S. Kolahi, R. Dssouli

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Scopus citations

Abstract

Capturing the behavior of a system by use cases have been intensively investigated in the last decade. The challenge is to find both the adequate model that fits the needs of the analyst and a formal composition mechanism which helps the generation of the expected behavior. In this paper, we propose a formal approach for specifying and composing use cases based on assignments. Those assignments are used to express new use cases. An assignment provides the join points and the composition operators that will be taken into account during the composition. These join points are, in fact, determined through a model checking step. They represent states where a property defined by the analyst holds. In order to evaluate these assignments, we define a composition mechanism based on the well known concept of synchronized product.

Original languageBritish English
Title of host publicationFormal Techniques for Networked and Distributed Systems - FORTE 2006 - 26th IFIP WG 6.1 International Conference, Proceedings
EditorsElie Najm, Jean-François Pradat-Peyre, Véronique Viguié Donzeau-Gouge
PublisherSpringer Verlag
Pages292-306
Number of pages15
ISBN (Print)3540462198, 9783540462194
DOIs
StatePublished - 2006
Event26th IFIP WG 6.1 International Conference - Paris, France
Duration: 26 Sep 200629 Sep 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4229 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th IFIP WG 6.1 International Conference
Country/TerritoryFrance
CityParis
Period26/09/0629/09/06

Keywords

  • Composition operators
  • Model checking
  • Synchronized product
  • Use cases

Fingerprint

Dive into the research topics of 'Composition of use cases using synchronization and model checking'. Together they form a unique fingerprint.

Cite this