Text size
  • Small
  • Medium
  • Large
Contrast
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Feature Interactions: A Mixed Semantic Model Approach

    1st Irish Workshop on Formal Methods

    Dublin, Ireland. 3rd - 4th July 1997

    AUTHORS

    P. Gibson, B. Mermet & D. Méry

    ABSTRACT

    The feature interaction problem is prominent in telephone service development. Many of the problems which arise when features combine are due to badly developed requirements models for individual features.

    With sufficiently good requirements models, in which each feature is formally modelled and validated against customer understanding, the feature interaction problem is much more tractable.

    Through a number of case studies, we have discovered that no one semantic framework is suitable for the synthesis and analysis of formal feature requirements models.

    Consequently we advocate a mixed-model approach. Firstly, we have an operational model, written in LOTOS using an object-based style, which is useful for constructing an executable model for validation.

    Secondly,we have a logical model (based on the B method) which is used to verify the state invariant properties of our system. Finally, we use TLA to provide semantics for a static analysis of liveness and fairness properties.

    No one model can treat each of these aspects, yet each of these aspects of the conceptualisation are necessary in the formal development of features. A simple example, in which we combine call forwarding and call screening features, illustrates the roles played by each of the models.

    PAPER FORMATS

    PDF filePDF Version of this Paper (143kb)