DeSpec: Modeling the Windows Driver Environment

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

DeSpec: Modeling the Windows Driver Environment

Original language description

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.

Czech name

—

Czech description

—

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2009

Confidentiality

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

Name of the periodical

Electronic Notes in Theoretical Computer Science

ISSN

1571-0661

e-ISSN

—

Volume of the periodical

Neuveden

Issue of the periodical within the volume

203

Country of publishing house

US - UNITED STATES

Number of pages

15

Pages from-to

—

UT code for WoS article

—

EID of the result in the Scopus database

—