DeSpec: Modeling the Windows Driver Environment11This work was partially supported by the Czech Academy of Sciences project 1ET400300504 and the Grant Agency of the Czech Republic project GD201/05/H014. | Zendy

Tomas Matousek | Zendy; Pavel Ježek | Zendy

Open Access

DeSpec: Modeling the Windows Driver Environment11This work was partially supported by the Czech Academy of Sciences project 1ET400300504 and the Grant Agency of the Czech Republic project GD201/05/H014.

Author(s) -

Tomas Matousek,

Pavel Ježek

Publication year - 2009

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2009.03.026

Subject(s) - czech , computer science , programming language , modeling language , kernel (algebra) , parameterized complexity , software engineering , agency (philosophy) , database , linguistics , algorithm , mathematics , philosophy , software , combinatorics , epistemology

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research