Feature Specification and Refinement with State Transition Diagrams

TL;DR

This paper introduces state transition diagrams (STDs) as a graphical specification method for feature interaction problems, providing formal refinement rules to add features and analyze conflicts systematically.

Contribution

It presents a formal semantics and refinement rules for STDs, enabling systematic feature addition and conflict detection in feature specifications.

Findings

Refinement rules formalize implementation relations.

Features are modeled as specific refinements.

Systematic development demonstrated on an example.

Abstract

In this paper, we introduce a graphic specification technique, called state transition diagrams (STD), and show the application to the feature interaction problem. Using a stream-based formal semantics, we provide refinement rules for STDs. Refinements define an implementation relation on STD specifications. We view features as particular refinements which add previously unspecified behavior to a given STD specification. The refinement relation is then used to add features, and to define the notion of conflicting features. Our techniques are demonstrated by a systematic development of an example given in [25].