| Attributes | Values |
|---|
| rdf:type
| |
| Description
| - Pro analýzu komponent verifikačními nástroji je vhodné popsat chování komponenty pomocí konečně-stavového modelu. To je vsak často nemožné v době návrhu komponenty, pokud tato používá neomezený paralelismus. V tomto případe totiž chování komponenty závisí na prostředí, ve kterém je komponenta používána, a pokrytí všech možných prostředí pak vede k nekonečně-stavovému modelu. V tomto článku navrhujeme řešení tohoto problému založené na myšlence transformace šablony chování na konkrétní model (template-to-model transformation): v době návrhu komponenty je chování popsáno tzv. šablonou chování, která je automaticky transformována v konkrétní model ve chvíli, kdy je komponenta nasazena v konkrétním prostředí. Tento konkrétní model je již konečně-stavový, a je proto vhodným vstupem verifikačních nástrojů. (cs)
- To use verification tools for reliability analysis of a software component, it is desirable to specify the behavior of the component by a finite-state model. This is often impossible at design time if the component practices unbounded parallelism. In that case, the behavior of the component widely depends on the environment the component is instantiated in. Unfortunately, covering all possible environments results in an infinite-state model. In this paper, we introduce a solution based on the concept of template-to-model transformation: at design time, a developer describes the behavior of the component by a behavior template, which is automatically transformed into a concrete behavior model when the component is instantiated in an environment. As the concrete behavior model is finite-state, it forms a suitable input for verification tools.
- To use verification tools for reliability analysis of a software component, it is desirable to specify the behavior of the component by a finite-state model. This is often impossible at design time if the component practices unbounded parallelism. In that case, the behavior of the component widely depends on the environment the component is instantiated in. Unfortunately, covering all possible environments results in an infinite-state model. In this paper, we introduce a solution based on the concept of template-to-model transformation: at design time, a developer describes the behavior of the component by a behavior template, which is automatically transformed into a concrete behavior model when the component is instantiated in an environment. As the concrete behavior model is finite-state, it forms a suitable input for verification tools. (en)
|
| Title
| - Verification of Software Components: Addressing Unbounded Paralelism
- Verification of Software Components: Addressing Unbounded Paralelism (en)
- Verifikace softwarových komponent: Neomezený paralelismus (cs)
|
| skos:prefLabel
| - Verification of Software Components: Addressing Unbounded Paralelism
- Verification of Software Components: Addressing Unbounded Paralelism (en)
- Verifikace softwarových komponent: Neomezený paralelismus (cs)
|
| skos:notation
| - RIV/67985807:_____/07:00307947!RIV08-AV0-67985807
|
| http://linked.open.../vavai/riv/strany
| |
| http://linked.open...avai/riv/aktivita
| |
| http://linked.open...avai/riv/aktivity
| - P(1ET400300504), Z(AV0Z10300504)
|
| http://linked.open...iv/cisloPeriodika
| |
| 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
| |
| http://linked.open...ai/riv/idVysledku
| - RIV/67985807:_____/07:00307947
|
| http://linked.open...riv/jazykVysledku
| |
| http://linked.open.../riv/klicovaSlova
| - software components; formal verification; unbounded parallelism (en)
|
| http://linked.open.../riv/klicoveSlovo
| |
| http://linked.open...odStatuVydavatele
| - US - Spojené státy americké
|
| http://linked.open...ontrolniKodProRIV
| |
| http://linked.open...i/riv/nazevZdroje
| - International Journal of Computer and Information Science
|
| 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...v/svazekPeriodika
| |
| http://linked.open...iv/tvurceVysledku
| |
| http://linked.open...n/vavai/riv/zamer
| |
| issn
| |
| number of pages
| |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)