This HTML5 document contains 45 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n17http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n19http://purl.org/net/nknouf/ns/bibtex#
n21http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n4http://linked.opendata.cz/resource/domain/vavai/projekt/
n9http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F67985807%3A_____%2F07%3A00091020%21RIV08-AV0-67985807/
n13http://linked.opendata.cz/ontology/domain/vavai/
n16http://linked.opendata.cz/resource/domain/vavai/zamer/
n7https://schema.org/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n11http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n20http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n12http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n8http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n14http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n6http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n18http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F67985807%3A_____%2F07%3A00091020%21RIV08-AV0-67985807
rdf:type
skos:Concept n13:Vysledek
dcterms: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. 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
dcterms:title
Ověřování chování softwarových komponent pomocí Behavior Protocols a Spinu Checking Software Component Behavior using Behavior Protocols and Spin Checking Software Component Behavior using Behavior Protocols and Spin
skos:prefLabel
Checking Software Component Behavior using Behavior Protocols and Spin Ověřování chování softwarových komponent pomocí Behavior Protocols a Spinu Checking Software Component Behavior using Behavior Protocols and Spin
skos:notation
RIV/67985807:_____/07:00091020!RIV08-AV0-67985807
n3:strany
1513;1517
n3:aktivita
n8:P n8:Z
n3:aktivity
P(1ET400300504), Z(AV0Z10300504)
n3:dodaniDat
n18:2008
n3:domaciTvurceVysledku
n21:1241230
n3:druhVysledku
n14:D
n3:duvernostUdaju
n20:S
n3:entitaPredkladatele
n9:predkladatel
n3:idSjednocenehoVysledku
413435
n3:idVysledku
RIV/67985807:_____/07:00091020
n3:jazykVysledku
n12:eng
n3:klicovaSlova
behavior protocols; Promela; behavior specification; verification
n3:klicoveSlovo
n11:Promela n11:behavior%20protocols n11:behavior%20specification n11:verification
n3:kontrolniKodProRIV
[08C5F75421D1]
n3:mistoKonaniAkce
Seoul
n3:mistoVydani
New York
n3:nazevZdroje
Proceedings of the 2007 ACM Symposium on Applied Computing
n3:obor
n6:JC
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
1
n3:projekt
n4:1ET400300504
n3:rokUplatneniVysledku
n18:2007
n3:tvurceVysledku
Kofroň, Jan
n3:typAkce
n17:WRD
n3:zahajeniAkce
2007-03-11+01:00
n3:zamer
n16:AV0Z10300504
s:numberOfPages
5
n19:hasPublisher
ACM
n7:isbn
1-59593-480-4