An interactive system operates by an ongoing communication between its components which send and receive messages on their input and output channels. Stream functions describe the component's input/output behaviour mapping input streams to output streams. State transition machines describe the component's state-based implementation. We adapt classical Mealy machines and classical Moore machines as needed for the state-based modelling of interactive components. As our main contribution, we compare the formal methods how to implement a stream function by a Mealy resp. a Moore style state transition machine in a correctness preserving way. Both transformations involve history abstractions which relate observable input streams with internal states. We compare the different implementation frameworks by constructing a Mealy style and a Moore style implementation for the same component. We illustrate the approach with a component which removes subsequent duplicate messages in an input stream which arose through stuttering.

The paper presents the top-down design of a synchronization component refining the communication- oriented input/output behaviour into a state-based implementation. The component constrains the flow of messages on two parallel communication channels to stay within a specified tolerance. The formal derivation uses transformations which are of general importance for the design of interactive components. The differentiation of the stream function localizes the effect of a single input with respect to previous input histories. The history abstraction extracts the component's state from the input histories. The design safely bridges different views of the synchronization component ranging from the stream based specification to the state based implementation.

This paper presents a formal method how to transform the structured signature of an algebraic specification into a collection of object-oriented class signatures. We discuss possible design decisions and formalize them as design mappings. The transformation of the signature forms the syntactic basis for relating algebraic specifications with object-oriented modeling in a profound way. The approach bridges the gap between functional specification concepts and object- oriented modeling techniques and contributes to a better understanding of object-oriented software construction. We illustrate the transformation with a characteristic example. All transformation procedures have been implemented in the ASIOS tool.

An interactive component consumes a stream of input messages and produces a stream of output messages. The input/output behaviour describes the service offered by the component without disclosing the implementation. In general, an interactive component provides the contracted service only for a subset of input histories, called its service domain. We investigate the input/output behaviour of interactive components for erroneous input streams outside the service domain. We specify a fault sensitive behaviour, a fault tolerant behaviour, a robust behaviour, and a fault correcting behaviour by enlarging the regular behaviour in a systematic way. We implement the different behaviours by state transition machines where we enlarge the regular state space by additional information. Altogether we provide schematic transformations both on the specification and on the implementation level how to extend the regular behaviour of an interactive component to input streams outside the service domain. The resulting formal method separates the aspects of service provision and error handling in an orthogonal way.

The paper studies the systematic design and implementation of interactive components whose input interface is enriched by undo commands. An undo command inverts the interaction history returning to a previously visited state. We formalize different policies for undo commands cancelling the most recent input, the most recent occurrence of a specified input, and the final history segment after a user defined checkpoint. For each undo policy, we specify the component's modified input/output behaviour in terms of the original behaviour as a function from input streams to output streams. Then we systematically transform the modified input/output behaviour into an implementation by a state transition machine. The resulting formal method extends the state transition table of an interactive component in a systematic way when its input interface is enriched by undo commands under different policies

A black box specification of a deterministic software or hardware component refers to the function mapping input histories to output histories. An important refinement step amounts to designing a state transition machine which correctly implements the specified behaviour. We present a formal method for implementing stream transformers by Moore state transition machines. First we construct a canonical Moore state transition machine whose state space is based on input histories. Then we identify output equivalent states for achieving a reduced Moore state transition machine. We illustrate the formal method with various applications

A combination of algebraic and object-oriented specification techniques may take advantage of both approaches for system development. This paper presents a formal method how to transform the signature of an algebraic specification into a collection of object-oriented class signatures in a systematic way. We explore the possible design decisions and manifest them in design functions. The transformation of the signature forms the syntactic basis for relating algebraic specifications with object-oriented modeling in a profound way. The approach bridges the gap between functional specification concepts and object-oriented modeling techniques. An important area of application comprises the top-down development of information storing components. All transformation procedures including the mechanization of the design choices have been implemented in a transformation tool.

The paper studies the top-down design of a basic interaction pattern for asynchronously communicating components. The interaction pattern describes a high level protocol where an active sender component transmits messages to a passive receiver component controlled by the receiver's acknowledgements. The formal design refines the components' input/output behaviour into a state-based implementation based on three transformation steps. An architectural refinement decomposes the protocol function into a sender component and into a receiver component introducing a feedback channel. The differentiation localizes the effect of single inputs wrt, a previous input history. The history abstraction extracts the components' control state and data state from the input history.

We present a framework for the unifying high-level synthesis of tree-structured and iterative combinational networks. Based on the theory of list homomorphisms, we develop a standard implementation for tree-structured modules processing the input digits in parallel. The design is systematically specialized to iterative networks processing the input sequentially from the least resp. from the highest significant positions. Throughout the paper, we explicate functional methods for the transformational design of combinational circuits. We illustrate the approach with a parity generator module, a comparator module, and a priority resolution module.