Interface Input/Output Automata: Splitting Assumptions from Guarantees

Publikation: Working paperForskning

90 Downloads (Pure)

Resumé

We propose a new look at one of the most fundamental types of behavioral interfaces: discrete time specifications of communication---directly related to the work of de Alfaro and Henzinger [3]. Our framework is concerned with distributed non-blocking asynchronous systems in the style of Lynch's \IOAs [11], relying on a context dependent notion of refinement based on relativized language inclusion. There are two main contributions of the work. First, we explicitly separate assumptions from guarantees, increasing the modeling power of the specification language and demonstrating an interesting relation between blocking and non-blocking interface frameworks. Second, our composition operator is systematically and formally derived from the requirements stated as a system of inequalities. The derived composed interfaces are maximal in the sense of behavior, or equivalently are the weakest in the sense of assumptions. Finally, we present a method for solving systems of inequalities as used in our setup.
OriginalsprogEngelsk
StatusUdgivet - 2006

Fingerprint

Specification languages
Specifications
Communication
Chemical analysis

Citer dette

@techreport{fd257f00037a11de82e6000ea68e967b,
title = "Interface Input/Output Automata: Splitting Assumptions from Guarantees",
abstract = "We propose a new look at one of the most fundamental types of behavioral interfaces: discrete time specifications of communication---directly related to the work of de Alfaro and Henzinger [3]. Our framework is concerned with distributed non-blocking asynchronous systems in the style of Lynch's \IOAs [11], relying on a context dependent notion of refinement based on relativized language inclusion. There are two main contributions of the work. First, we explicitly separate assumptions from guarantees, increasing the modeling power of the specification language and demonstrating an interesting relation between blocking and non-blocking interface frameworks. Second, our composition operator is systematically and formally derived from the requirements stated as a system of inequalities. The derived composed interfaces are maximal in the sense of behavior, or equivalently are the weakest in the sense of assumptions. Finally, we present a method for solving systems of inequalities as used in our setup.",
author = "Larsen, {Kim Guldstrand} and Ulrik Nyman and Andrzej Wasowski",
year = "2006",
language = "English",
type = "WorkingPaper",

}

TY - UNPB

T1 - Interface Input/Output Automata: Splitting Assumptions from Guarantees

AU - Larsen, Kim Guldstrand

AU - Nyman, Ulrik

AU - Wasowski, Andrzej

PY - 2006

Y1 - 2006

N2 - We propose a new look at one of the most fundamental types of behavioral interfaces: discrete time specifications of communication---directly related to the work of de Alfaro and Henzinger [3]. Our framework is concerned with distributed non-blocking asynchronous systems in the style of Lynch's \IOAs [11], relying on a context dependent notion of refinement based on relativized language inclusion. There are two main contributions of the work. First, we explicitly separate assumptions from guarantees, increasing the modeling power of the specification language and demonstrating an interesting relation between blocking and non-blocking interface frameworks. Second, our composition operator is systematically and formally derived from the requirements stated as a system of inequalities. The derived composed interfaces are maximal in the sense of behavior, or equivalently are the weakest in the sense of assumptions. Finally, we present a method for solving systems of inequalities as used in our setup.

AB - We propose a new look at one of the most fundamental types of behavioral interfaces: discrete time specifications of communication---directly related to the work of de Alfaro and Henzinger [3]. Our framework is concerned with distributed non-blocking asynchronous systems in the style of Lynch's \IOAs [11], relying on a context dependent notion of refinement based on relativized language inclusion. There are two main contributions of the work. First, we explicitly separate assumptions from guarantees, increasing the modeling power of the specification language and demonstrating an interesting relation between blocking and non-blocking interface frameworks. Second, our composition operator is systematically and formally derived from the requirements stated as a system of inequalities. The derived composed interfaces are maximal in the sense of behavior, or equivalently are the weakest in the sense of assumptions. Finally, we present a method for solving systems of inequalities as used in our setup.

M3 - Working paper

BT - Interface Input/Output Automata: Splitting Assumptions from Guarantees

ER -