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%2F00216208%3A11320%2F08%3A00101298" target="_blank" >RIV/00216208:11320/08:00101298 - isvavai.cz</a>

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. Real-life component applications often involve complex interaction patterns like callbacks and autonomous activities, which have to be considered by the model of environment's behavior. In general, such patterns can be properly modeled only by a formalism that (i) supports independent atomic events for methodinvocation and return from a method and (ii) allows to specify explicit interleaving of events on component's provided and required interfaces - the formalism of behavior protocols satisfies these requirements. This paper attempts to answer the questionwhether the model involving only events on provided interfaces (calling protocol) could be valid under certain constraints on component behavior. The key contribution are the constraints on interleaving of events related to callbacks and

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 (domněnka-záruka), kde domněnka modeluje chování prostředí pro každou komponentu. Realistické komponentové aplikace často zahrnují složité vzory komunikace jako callbacky a autonomní aktivity, které musejí být brány v úvahu modelem chování prostředí. Obecně, takové vzory 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 metoda (ii) dovoluje specifikaci explicitních proložení událostí na poskytovaných a požadovaných rozhraních komponenty - formalismus protokolů chování splňuje tyto požadavky. Tento článek se pokouší zodpovědět otázku, jestli 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í s

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

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

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>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ů

Name of the periodical

Lecture Notes in Business Information Processing

ISSN

1865-1348

e-ISSN

—

Volume of the periodical

11

Issue of the periodical within the volume

Neuveden

Country of publishing house

DE - GERMANY

Number of pages

20

Pages from-to

—

UT code for WoS article

000257465300002

EID of the result in the Scopus database

—