DeSpec: Modeling the Windows Driver Environment

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


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.




Matousek, T., & Jezek, P. (2009). DeSpec: Modeling the Windows Driver Environment. Electronic Notes in Theoretical Computer Science, 203(7), 55–69.

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