About: Checking Software Component Behavior using Behavior Protocols and Spin     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

AttributesValues
rdf:type
Description
  • sing software components is a modern approach for building extensible and reliable applications. To ensure high dependability, a component application should undergo verification, e.g. model checking, to prove it has certain properties. The implementation of an application is usually too complex to be verified at a formal level; therefore, a model being an abstraction of the implementation is to be used. Behavior protocols are a platform for modeling of software component behavior. In this paper, we propose a method for translation behavior protocols to Promela, which is consequently used as the input for the Spin model checker. Having the Promela code describing the component behavior, one can efficiently check for the behavior compatibility and LTL (Linear Temporal Logic) properties of cooperating software components.
  • sing software components is a modern approach for building extensible and reliable applications. To ensure high dependability, a component application should undergo verification, e.g. model checking, to prove it has certain properties. The implementation of an application is usually too complex to be verified at a formal level; therefore, a model being an abstraction of the implementation is to be used. Behavior protocols are a platform for modeling of software component behavior. In this paper, we propose a method for translation behavior protocols to Promela, which is consequently used as the input for the Spin model checker. Having the Promela code describing the component behavior, one can efficiently check for the behavior compatibility and LTL (Linear Temporal Logic) properties of cooperating software components. (en)
  • Používání softwarových komponent patří k moderním přístupům k vytváření rozšiřitelných a spolehlivých aplikací. K zajištění vysoké spolehlivost by komponentová aplikace měla být verifikována, např. podstoupit model checking. Implementace aplikace je většinou příliš složitá, než aby mohla být verifikována na formální úrovni. Proto se používá model, který je abstrakcí této implementace. Behavior Protocols jsou platformou pro modelování chování softwarových komponent. V tomto článku navrhujeme metodu pro překlad specifikace Behavior Protocols do Promely, která je následně použita jako vstup pro model checker Spin. Pokud máme model v jazyku Promela popisující chování komponent, můžeme efektivně ověřovat kompatibilitu i LTL vlastnosti kooperujících komponent (cs)
Title
  • Checking Software Component Behavior using Behavior Protocols and Spin
  • Ověřování chování softwarových komponent pomocí Behavior Protocols a Spinu (cs)
  • Checking Software Component Behavior using Behavior Protocols and Spin (en)
skos:prefLabel
  • Checking Software Component Behavior using Behavior Protocols and Spin
  • Ověřování chování softwarových komponent pomocí Behavior Protocols a Spinu (cs)
  • Checking Software Component Behavior using Behavior Protocols and Spin (en)
skos:notation
  • RIV/67985807:_____/07:00091020!RIV08-AV0-67985807
http://linked.open.../vavai/riv/strany
  • 1513;1517
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • P(1ET400300504), Z(AV0Z10300504)
http://linked.open...vai/riv/dodaniDat
http://linked.open...aciTvurceVysledku
http://linked.open.../riv/druhVysledku
http://linked.open...iv/duvernostUdaju
http://linked.open...titaPredkladatele
http://linked.open...dnocenehoVysledku
  • 413435
http://linked.open...ai/riv/idVysledku
  • RIV/67985807:_____/07:00091020
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • behavior protocols; Promela; behavior specification; verification (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...ontrolniKodProRIV
  • [08C5F75421D1]
http://linked.open...v/mistoKonaniAkce
  • Seoul
http://linked.open...i/riv/mistoVydani
  • New York
http://linked.open...i/riv/nazevZdroje
  • Proceedings of the 2007 ACM Symposium on Applied Computing
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...cetTvurcuVysledku
http://linked.open...vavai/riv/projekt
http://linked.open...UplatneniVysledku
http://linked.open...iv/tvurceVysledku
  • Kofroň, Jan
http://linked.open...vavai/riv/typAkce
http://linked.open.../riv/zahajeniAkce
http://linked.open...n/vavai/riv/zamer
number of pages
http://purl.org/ne...btex#hasPublisher
  • ACM
https://schema.org/isbn
  • 1-59593-480-4
Faceted Search & Find service v1.16.118 as of Jun 21 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 47 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software