Hierarchical specification of reactive systems: a case study

A development strategy is proposed which bases the specification of a reactive system on the description of its environment. This approach has numerous advantages: easier validation of the specification, availability of suitable modeling languages, and simulation of the environment during the testing phase of the product. The specification of the environment is expressed in the STATECHARTS formalism. It is developed in a top-down manner. This top-down approach calls for the enhancement of the STATECHART by a transition refinement construct. The development of an actual case study, i.e. development of the specification for a data transfer problem, demonstrates the methodological approach and shows the usefulness of this extension of the formalism. It also results in further development guidelines