About: Partial Verification of Software Components: Heuristics for Environment Construction

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Partial Verification of Software Components: Heuristics for Environment Construction 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)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single component typically comprises a smaller state space than the whole system. We present a technique that addresses the problem of state explosion in code checking of primitive components with the Java PathFinder in case the checked property is absence of concurrency errors. The key idea is to reduce parallelism in the calling protocol on the basis of the information provided by static analysis searching for concurrency-related patterns in the component code; by a heuristic, some of the pattern instances are denoted as ?suspicious?. Then, the environment (needed to be available since Java PathFinder checks only complete programs) is generated from a reduced calling protocol so that it exercises in parallel only those parts of the component?s code that likely contain concurrency errors. Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single component typically comprises a smaller state space than the whole system. We present a technique that addresses the problem of state explosion in code checking of primitive components with the Java PathFinder in case the checked property is absence of concurrency errors. The key idea is to reduce parallelism in the calling protocol on the basis of the information provided by static analysis searching for concurrency-related patterns in the component code; by a heuristic, some of the pattern instances are denoted as ?suspicious?. Then, the environment (needed to be available since Java PathFinder checks only complete programs) is generated from a reduced calling protocol so that it exercises in parallel only those parts of the component?s code that likely contain concurrency errors. (en)
Title	Partial Verification of Software Components: Heuristics for Environment Construction Partial Verification of Software Components: Heuristics for Environment Construction (en)
skos:prefLabel	Partial Verification of Software Components: Heuristics for Environment Construction Partial Verification of Software Components: Heuristics for Environment Construction (en)
skos:notation	RIV/00216208:11320/07:10084053!RIV11-MSM-11320___
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(1ET400300504), P(GA201/06/0770), Z(AV0Z10300504), Z(MSM0021620838)
http://linked.open...vai/riv/dodaniDat	2011
http://linked.open...aciTvurceVysledku	Parízek, Pavel Plášil, František
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Univerzita Karlova v Praze / Matematicko-fyzikální fakulta
http://linked.open...dnocenehoVysledku	440697
http://linked.open...ai/riv/idVysledku	RIV/00216208:11320/07:10084053
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	concurrency errors; model checking; software components (en)
http://linked.open.../riv/klicoveSlovo	concurrency errors model checking software components
http://linked.open...ontrolniKodProRIV	[4C09EC61FD0B]
http://linked.open...v/mistoKonaniAkce	Lubeck, Germany
http://linked.open...i/riv/mistoVydani	Neuveden
http://linked.open...i/riv/nazevZdroje	33rd EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA)
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	2 (xsd:int)
http://linked.open...cetTvurcuVysledku	2 (xsd:int)
http://linked.open...vavai/riv/projekt	Formal methods applicable to development of component-based systems Realistic application of formal methods in component systems
http://linked.open...UplatneniVysledku	2007
http://linked.open...iv/tvurceVysledku	Parízek, Pavel Plášil, František
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2007-08-28 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Informatika pro informační společnost: modely, algoritmy, aplikace Moderní metody, struktury a systémy informatiky
number of pages	8 (xsd:int)
http://purl.org/ne...btex#hasPublisher	IEEE Computer Society
https://schema.org/isbn	0-7695-2977-1
http://localhost/t...ganizacniJednotka	11320

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

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, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software