Počet záznamů: 1

Making Components Fit: SPINing

  1. 1.
    0334272 - UIVT-O 2010 RIV US eng C - Konferenční příspěvek (zahraniční konf.)
    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]
    Grant CEP: GA ČR(CZ) GD201/05/H014
    Grant ostatní:GA ČR(CZ) GA201/06/0770
    Program:GA
    Výzkumný záměr: CEZ:AV0Z10300504
    Klíčová slova: software components * behavior specification * model-checking
    Kód oboru RIV: JC - Počítačový hardware a 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.
    Trvalý link: http://hdl.handle.net/11104/0179054