Behavioral refinement of non-deterministic state transition diagrams based on behavior elimination
Christian Prehofer, Peter Scholz · 2013
We consider semantic refinement of behavioral models represented as state transition diagrams (SD). The idea is to start with a base model and then to add small features, represented as extension of SDs, adding previously unspecified behavior. These features may add new states and transitions or refine existing transitions. We develop an expressive formal framework for behavioral refinements of non-deterministic SDs based on input/output event traces. We generalize existing kinds of refinements to a new concept based on eliminations on the trace level. These eliminations remove the added behavior and we establish behavior preserving refinement relations based on this. We present several cases for refinement which preserve different properties. Furthermore, we show how to combine refinements and discuss what properties are preserved.