DeSpec: Modeling the Windows Driver Environment
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F09%3A00207472" target="_blank" >RIV/00216208:11320/09:00207472 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
DeSpec: Modeling the Windows Driver Environment
Popis výsledku v původním jazyce
This paper introduces a new object-oriented specification and modeling language called DeSpec. The language targets primarily model checking in the Windows NT kernel driver environment. It integrates the majority of Zing modeling language features and adds means for defining parameterized abstractions of the environment at varying levels of detail. The DeSpec language also enables capturing constrains imposed on drivers by the Windows kernel in a form of quantified temporal logic patterns - easy-to-readtemplates of LTL formulae introduced by the Bandera toolset.
Název v anglickém jazyce
DeSpec: Modeling the Windows Driver Environment
Popis výsledku anglicky
This paper introduces a new object-oriented specification and modeling language called DeSpec. The language targets primarily model checking in the Windows NT kernel driver environment. It integrates the majority of Zing modeling language features and adds means for defining parameterized abstractions of the environment at varying levels of detail. The DeSpec language also enables capturing constrains imposed on drivers by the Windows kernel in a form of quantified temporal logic patterns - easy-to-readtemplates of LTL formulae introduced by the Bandera toolset.
Klasifikace
Druh
J<sub>x</sub> - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2009
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název periodika
Electronic Notes in Theoretical Computer Science
ISSN
1571-0661
e-ISSN
—
Svazek periodika
Neuveden
Číslo periodika v rámci svazku
203
Stát vydavatele periodika
US - Spojené státy americké
Počet stran výsledku
15
Strana od-do
—
Kód UT WoS článku
—
EID výsledku v databázi Scopus
—