Making Components Fit: SPINing

0334272 - ÚI 2010 RIV US eng C - Conference Paper (international conference)
Kofroň, Jan - Poch, T. - Šerý, O.
Making Components Fit: SPINing.
[Komponenty ve formě: SPINing.]
Proceedings of 32th IEEE/NASA Software Engineering Workshop. Los Alamitos: IEEE Computer Society, 2009, s. 65-74. ISBN 978-0-7695-3617-0.
[SEW 2008. Annual IEEE/NASA Software Engineering Workshop /32./. Kassandra (GR), 15.10.2008-16.10.2008]
R&D Projects: GA ČR(CZ) GD201/05/H014
Grant - others:GA ČR(CZ) GA201/06/0770
Program: GA
Institutional research plan: CEZ:AV0Z10300504
Keywords : software components * behavior specification * model-checking
Subject RIV: JC - Computer Hardware ; Software

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.

S rostoucí popularitou tvorby aplikací skládáním ze znovupoužitelných komponent je stále více třeba zajišťovat korektnost výsledné aplikace. Na jedné straně toto vyžaduje formální popis komponent. Na straně druhé pak existenci patřičných nástrojů. V tomto článku popisujeme formalismus Extended Behavior Protocols a nástroje pro verifikaci korektnosti komponentové aplikace. Výhodou zvoleného přístupu je použití dobře testovaného model checkeru Spin. Zmiňujeme také naše zkušenosti s aplikací popsaného postupu a nástroje.
Permanent Link: http://hdl.handle.net/11104/0179054