Making Components Fit: SPINing

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F09%3A00207424" target="_blank" >RIV/00216208:11320/09:00207424 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/67985807:_____/09:00334272

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Making Components Fit: SPINing

Popis výsledku v původním jazyce

The more popular it is to build an application from reusable software components, the more desperate is the need for showing correctness of such a composition. This requires on one hand, being able to formally specify behavior of software components, while, on the other hand, providing appropriate tool support for verification of correctness of the composition. In this paper, we suggest use of the formalism of Extended Behavior Protocols and present a tool chain for verification of composition correctness of component applications. The advantage of the proposed approach is using a well-tested and supported model checker Spin as a backend. As a proof of the concept, we share our experience with application of the method.

Název v anglickém jazyce

Making Components Fit: SPINing

Popis výsledku anglicky

The more popular it is to build an application from reusable software components, the more desperate is the need for showing correctness of such a composition. This requires on one hand, being able to formally specify behavior of software components, while, on the other hand, providing appropriate tool support for verification of correctness of the composition. In this paper, we suggest use of the formalism of Extended Behavior Protocols and present a tool chain for verification of composition correctness of component applications. The advantage of the proposed approach is using a well-tested and supported model checker Spin as a backend. As a proof of the concept, we share our experience with application of the method.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2009

Kód důvěrnosti údajů

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

Název statě ve sborníku

32nd Annual IEEE Software Engineering Workshop

ISBN

978-0-7695-3617-0

ISSN

—

e-ISSN

—

Počet stran výsledku

10

Strana od-do

—

Název nakladatele

IEEE Computer Society

Místo vydání

—

Místo konání akce

Neuveden

Datum konání akce

1. 1. 2009

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—