Zusammenfassung
Relating formal refinement techniques with commercial object-oriented software development methods is important to achieve enhancement of the power and flexibility of these software development methods- and tools. We will present an automata model together with a denotational and an operational semantics to describe the behavior of objects. Based on the given semantics, we define a set of powerful refinement rules, and discuss their applicability in software engineering practice, especially with the use of inheritance.