Automata Describing Object Behavior

TL;DR

This paper introduces an automata-based model with formal semantics to describe object behavior, aiming to bridge formal refinement techniques with object-oriented software development for improved flexibility.

Contribution

It presents a novel automata model with formal semantics and refinement rules tailored for object-oriented development, emphasizing inheritance.

Findings

Automata model effectively describes object behavior.

Refinement rules enhance software development flexibility.

Semantics facilitate formal reasoning about object-oriented systems.

Abstract

Relating formal re nement techniques with commercial object oriented software development methods is important to achieve enhancement of the power and exibility 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 de ne a set of powerful re nement rules and discuss their applicability in software engineering practice especially with the use of inheritance.