DeSpec: Modeling the Windows Driver Environment

0Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.

Abstract

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-read templates of LTL formulae introduced by the Bandera toolset. © 2009 Elsevier B.V. All rights reserved.

Cite

CITATION STYLE

APA

Matousek, T., & Jezek, P. (2009). DeSpec: Modeling the Windows Driver Environment. Electronic Notes in Theoretical Computer Science, 203(7), 55–69. https://doi.org/10.1016/j.entcs.2009.03.026

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free