Assume-Guarantee Verification of Software Components in SOFA 2 Framework

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F10%3A10025355" target="_blank" >RIV/00216208:11320/10:10025355 - isvavai.cz</a>
Alternative codes found
RIV/67985807:_____/10:00334355
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
Assume-Guarantee Verification of Software Components in SOFA 2 Framework
Original language 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. For practical purposes it is sufficient to capture in the environment 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. We show the benefits of our approach on results of experiments with a non-trivial software system.
Czech name
—
Czech description
—

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—

Project
<a href="/en/project/1ET400300504" target="_blank" >1ET400300504: Realistic application of formal methods in component systems</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year
2010
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)