Abstrakt
Tento článek se zabývá novým objektově orientovaným specifikačním a modelovacím jazykem DeSpec. Cílem jazyka je hlavně možnost modelování ovladačů zařízení v prost ředí Windows NT.
DeSpec v sobě integruje většinu modelovacích schopností jazyka Zing a přidává možnosti tvorby parametrizovaných abstrakcí na různých úrovních detailu. Zároveň je také umožněno zapisování formálních požadavků, vyžadovaných jádrem Windows na ovladačích zařizení, ve formě šablon formulí temporální logiky - s využitím snadno pochopitelných šablon LTL formulí poprvé použitých v projektu Bandera.