About: Assume-Guarantee Verification of Software Components in SOFA 2 Framework

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

About: Assume-Guarantee Verification of Software Components in SOFA 2 Framework 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	A key problem in compositional model checking of software systems is that typical model checkers accept only closed systems (runnable programs) and therefore a component cannot be model-checked directly. A typical solution is to create an artificial environment for the component such that composition of them forms a runnable program that can be model-checked. While it is possible to create a universal environment that performs all possible sequences and interleavings of calls of the component’s methods, for practical purposes it is sufficient to capture in this way just the use of the component in a particular software system – this idea is expressed by the paradigm of assume-guarantee reasoning. In this paper, we present our approach to assume-guarantee-based verification of software systems in the context of the SOFA 2 component framework. A key problem in compositional model checking of software systems is that typical model checkers accept only closed systems (runnable programs) and therefore a component cannot be model-checked directly. A typical solution is to create an artificial environment for the component such that composition of them forms a runnable program that can be model-checked. While it is possible to create a universal environment that performs all possible sequences and interleavings of calls of the component’s methods, for practical purposes it is sufficient to capture in this way just the use of the component in a particular software system – this idea is expressed by the paradigm of assume-guarantee reasoning. In this paper, we present our approach to assume-guarantee-based verification of software systems in the context of the SOFA 2 component framework. (en)
Title	Assume-Guarantee Verification of Software Components in SOFA 2 Framework Assume-Guarantee Verification of Software Components in SOFA 2 Framework (en)
skos:prefLabel	Assume-Guarantee Verification of Software Components in SOFA 2 Framework Assume-Guarantee Verification of Software Components in SOFA 2 Framework (en)
skos:notation	RIV/67985807:_____/10:00334355!RIV11-AV0-67985807
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(1ET400300504), Z(AV0Z10300504), Z(MSM0021620838)
http://linked.open...iv/cisloPeriodika	3
http://linked.open...vai/riv/dodaniDat	2011
http://linked.open...aciTvurceVysledku	Plášil, František
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
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	Ústav informatiky AV ČR, v. v. i.
http://linked.open...dnocenehoVysledku	247975
http://linked.open...ai/riv/idVysledku	RIV/67985807:_____/10:00334355
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	components; software verification; model checking (en)
http://linked.open.../riv/klicoveSlovo	software verification components model checking
http://linked.open...odStatuVydavatele	GB - Spojené království Velké Británie a Severního Irska
http://linked.open...ontrolniKodProRIV	[4A72555F1C09]
http://linked.open...i/riv/nazevZdroje	IET Software
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	2 (xsd:int)
http://linked.open...vavai/riv/projekt	Realistic application of formal methods in component systems
http://linked.open...UplatneniVysledku	2010
http://linked.open...v/svazekPeriodika	4
http://linked.open...iv/tvurceVysledku	Plášil, František Parízek, P.
http://linked.open...ain/vavai/riv/wos	000279258600004
http://linked.open...n/vavai/riv/zamer	Informatika pro informační společnost: modely, algoritmy, aplikace Moderní metody, struktury a systémy informatiky
issn	1751-8806
number of pages	12 (xsd:int)
is http://linked.open...avai/riv/vysledek of	Assume-Guarantee Verification of Software Components in SOFA 2 Framework Assume-Guarantee Verification of Software Components in SOFA 2 Framework Assume-Guarantee Verification of Software Components in SOFA 2 Framework

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