Abstract

Although a significant body of research in the area of formal verification and model checking tools of software and hardware systems exists, the acceptance of these tools by industry and end-users is rather limited. Beside the technical problem of state space explosion, one of the main reasons for this limited acceptance is the unfamiliarity of users with the required specification notation. Requirements have to be typically expressed as temporal logic formalisms and notations. Property specification patterns were successfully introduced to bridge this gap between users and model checking tools. They also enable non-experts to write formal specifications that can be used for automatic model checking. In this paper, we propose an abstract high level pattern-based approach to the description of property specifications based on Use Case Maps (UCM). We present a set of commonly used properties with their specifications that are described in terms of occurrence, ordering and temporal scopes of actions. Furthermore, our approach also supports the description of properties with respect to their architectural scope. We provide a mapping of our UCM property specification patterns in terms of CTL, TCTL and Architectural TCTL (ArTCTL), an extension to TCTL, introduced in this research that provides temporal logics with architectural scopes. We illustrate the use of our pattern system for requirement specifications of an IP Header compression feature.

-- DanielAmyot - 05 Nov 2009

Discussion

  • Please contact Jameleddine Hassine <jhassine@hotmail.com> to get a copy of the paper.
  • Please feel free to discuss this article directly on this page. Constructive comments are welcomed! Please sign your TWiki name.

FormForVirtualLibrary edit

Title Use Case Maps as a property specification language
Authors J. Hassine, J. Rilling, R. Dssouli
Type Journal
Conference/Journal Title Software and Systems Modeling
Volume/Number 8(2)
Editors
Publisher Springer
Month April
Year 2009
Pages 205-220
DOI 10.1007/s10270-007-0076-6
Keywords Formal verification, Temporal logic, Property specification, Use Case Maps, Temporal and architectural scope
Topic revision: r2 - 05 Nov 2009, DanielAmyot
This site is powered by FoswikiCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding Foswiki? Send feedback