Modeling of Component Environment in Presence of Callbacks and Autonomous Activities

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F08%3A00317215" target="_blank" >RIV/67985807:_____/08:00317215 - isvavai.cz</a>

Alternative codes found

RIV/00216208:11320/08:00206201

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Modeling of Component Environment in Presence of Callbacks and Autonomous Activities

Original language description

A popular approach to compositional verification of component-based applications is based on the assume-guarantee paradigm, where an assumption models behavior of an environment for each component. Component applications often involve complex interactionpatterns such as callbacks and autonomous activities that can be properly modeled only by a formalism that (i) supports independent atomic events for method invocation and return from a method and (ii) allows to specify interleaving of events on component's provided and required interfaces. This paper attempts to answer the question whether a model involving only events on provided interfaces (calling protocol) could be valid under certain constraints on component behavior. The key contribution are theconstraints on interleaving of events related to callbacks and autonomous activities, which are expressed via syntactical patterns, and evaluation of the proposed constraints on real-life component applications.

Czech name

Modelování komponentového prostředí za výskytu zpětných volání a autonomních aktivit

Czech description

Populární přístup ke kompoziční verifikaci komponentových aplikací je založen na principu assume-guarantee (předpoklad-záruka), kde předpoklad modeluje chování prostředí pro každou komponentu. Realistické komponentové aplikace často zahrnují složité vzory komunikace jako callbacky a autonomní aktivity, které mohou být přesně modelovány pouze formalismem, který (i) podporuje nezávislé atomické události pro volání metod a návraty z metod a (ii) dovoluje specifikaci explicitních proložení událostí na poskytovaných a požadovaných rozhraních komponenty. Tento článek se pokouší zodpovědět otázku, zda model zahrnující pouze události na poskytovaných rozhraních (volací protokol) může být korektní při nějakých omezeních na chování komponent. Hlavním přínosem jsou omezení na proložení událostí vztažených ke callbackům a autonomním aktivitám, které jsou vyjádřeny pomocí syntaktických vzorů, a zhodnocení navržených omezení na realistických komponentových aplikacích.

Type

D - Article in proceedings

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

<a href="/en/project/GA201%2F06%2F0770" target="_blank" >GA201/06/0770: Formal methods applicable to development of component-based systems</a><br>

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2008

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Objects, Components, Models and Patterns

ISBN

978-3-540-69823-4

ISSN

—

e-ISSN

—

Number of pages

20

Pages from-to

—

Publisher name

Springer-Verlag

Place of publication

Berlin

Event location

Zurich

Event date

Jun 30, 2008

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000257465300002