Modeling techniques in design-by-refinement methodologies

Embedded system design methodologies that are based on the effective use of multiple levels of abstraction hold promise for substantial productivity gains. Starting the design process at a high level of abstraction improves control over the design and facilitates verification and synthesis. In particular, if we use a rigorous approach to link the levels of abstraction, we can establish properties of lower levels from analysis at higher levels. This process goes by the name of "design by refinement". To maximize its benefit, design by refinement requires a formal semantic foundation that supports a wide range of levels of abstraction. We introduce such a semantic foundation and describe how it can integrate several models for reactive systems.