Deriving State-Based Implementations of Interactive Components with History Abstractions

Abstract

The external behaviour of an interactive component refers to the communication histories on the input and output channels. The component's implementation employs an internal state where inputs effect output and an update of the state. The black-box view is modelled by a stream processing function from input to output streams, the glass-box view by a state transition machine. We present a formal method how to implement a stream processing function with several arguments by a state transition machine in a correctness preserving way. The transformation involves two important steps, called differentiation and history abstraction. The differentiation localizes the effect of a single input on one of the input channels wrt. the previous input histories. The history abstraction introduces states as congruence classes of input histories. We extend our previous results from interactive components with one input channel to components with several input channels. The generalization employs a 'diamond property' for states and outputs which ensures the confluence of the resulting state transition system.

Original languageEnglish
Title of host publicationPSI 2006: Perspectives of Systems Informatics
Number of pages15
Volume4378 LNCS
PublisherSpringer Verlag
Publication date01.12.2007
Pages180-194
ISBN (Print)978-3-540-70880-3
ISBN (Electronic)978-3-540-70881-0
DOIs
Publication statusPublished - 01.12.2007
Event6th International Andrei Ershov Memorial Conference on Perspectives of Systems Informatics - Novosibirsk, Rwanda
Duration: 27.06.200730.06.2007
Conference number: 71131

Fingerprint

Dive into the research topics of 'Deriving State-Based Implementations of Interactive Components with History Abstractions'. Together they form a unique fingerprint.

Cite this