Feature Specification and Refinement with State Transition Diagrams
This work addresses feature interaction issues in software specification, but it appears incremental as it builds on existing formal methods without broad new breakthroughs.
The paper tackles the feature interaction problem by introducing state transition diagrams (STD) as a graphic specification technique, using a stream-based formal semantics to define refinement rules and an implementation relation for adding features and identifying conflicts, demonstrated through a systematic example development.
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].