Object-based abstract state machines

When designing and implementing complex computer systems, powerful description techniques are needed that allow the representation of hardware and software components at various abstraction levels and support reenement during the development process. These techniques should be formal in order to support mathematical reasoning about systems properties while at the same time they should be operational so as to facilitate comprehension and implementation of the system. In this paper we propose Object-based Abstract State Machines (ObASM), an extension of Abstract State Machines (ASM). ASM are an operational formalism that has been successfully applied to the description of hardware and software systems. ObASM are adding a notion of locality of state and the concept of communication between loosely coupled agents. These extensions are designed to be minimal additions to the traditional ASM formulation, preserving their simplicity while at the same time signiicantly enhancing their modeling power. We give a formal semantics for ObASMs and discuss the properties of the extended formalism