Tool support for composition and verification of formal behavior

Siamak Kolahi, Aziz Salah, Rabeb Mizouni, Rachida Dssouli

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

1 Scopus citations

Abstract

In this paper, we present a tool support for formal modeling, automated composition, and formal verification of partial system behaviors described as Use Case Automata (UCAs). The tool, called UCOMV, supports visual modeling of formal behaviors and their merging through the notion of composition expressions. These expressions specify the extension points in the UCAs where the composition is performed, as well as the semantics of the intended composition. UCOMV supports a new incremental approach of building the desired behavioral model by using a formal automated mechanism of composition. In addition, it allows the verification of UCAs over behavioral properties defined as temporal property specifications.

Original languageBritish English
Title of host publicationInnovations'07
Subtitle of host publication4th International Conference on Innovations in Information Technology, IIT
PublisherIEEE Computer Society
Pages471-475
Number of pages5
ISBN (Print)9781424418411
DOIs
StatePublished - 2007
EventInnovations'07: 4th International Conference on Innovations in Information Technology, IIT - Dubai, United Arab Emirates
Duration: 18 Nov 200720 Nov 2007

Publication series

NameInnovations'07: 4th International Conference on Innovations in Information Technology, IIT

Conference

ConferenceInnovations'07: 4th International Conference on Innovations in Information Technology, IIT
Country/TerritoryUnited Arab Emirates
CityDubai
Period18/11/0720/11/07

Keywords

  • Automated composition
  • Behavioral modeling
  • Formal verification
  • Use case automata

Fingerprint

Dive into the research topics of 'Tool support for composition and verification of formal behavior'. Together they form a unique fingerprint.

Cite this