Publication at Faculty of Mathematics and Physics |
2009
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.