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
| Autor: | Pavel Jezek, Tomas Matousek |
|---|---|
| Rok vydání: | 2009 |
| Předmět: |
Model checking
Czech Windows NT General Computer Science Programming language Modeling language Computer science Specification language Windows kernel drivers computer.software_genre model checking language.human_language Theoretical Computer Science Kernel (statistics) Agency (sociology) language verification computer specification language Computer Science(all) |
| Zdroj: | Electronic Notes in Theoretical Computer Science. 203:55-69 |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2009.03.026 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect