Wat is het VDM-bestandsformaat?
.vdm is een ontwikkelingsbestandsformaat dat wordt gebruikt voor het opslaan van broncode geschreven in de specificatietalen VDM-SL of VDM++. Een .vdm-bestand is platte tekst en kan worden bewerkt met elke teksteditor. VDM-bestanden slaan formele specificaties op die een model van een computersysteem beschrijven. Het gebruik van VDM-specificatiebestanden stelt ontwerpers in staat om een overzicht op hoog niveau van het systeem te krijgen - een overzicht dat moeilijker te verkrijgen is door alleen de broncode van de implementatie te bestuderen. VDM-bestanden kunnen ook dienen als basis voor het genereren van codecomponenten.
Vienna Development Method
De VDM-standaard werd in de jaren 70 ontwikkeld in het Weense laboratorium van IBM en is een van de oudste formele methoden voor de ontwikkeling van computersystemen. VDM-SL werd in 1996 gestandaardiseerd als ISO/IEC 13817-1. Het werd verder uitgebreid om objectgeoriënteerd modelleren te ondersteunen, wat resulteerde in de VDM++-standaard, die ook .vdm-bestanden gebruikt. Een derde dialect, VDM-RT, breidt VDM++ uit voor real-time en gedistribueerde systemen. De taal wordt toegepast in veiligheidskritische domeinen, waaronder het ontwerp van besturingssystemen, compilers, luchtvaartsoftware en besturingssystemen voor medische apparatuur.
De primaire open-source toolset is de Overture Tool, een op Eclipse gebaseerde IDE die actief wordt onderhouden door de gemeenschap en wordt gebruikt in EU-onderzoeks- en industriële projecten. Sommige tools gebruiken de alternatieve extensies .vdmsl en .vdmpp om de twee belangrijkste dialecten te onderscheiden.
Beveiliging & veiligheid
RISICO: LOWPlatte tekst broncodebestanden; geen uitvoerbare inhoud. Geen bekende malware-vector.
Formaatdetails
in een notendop- VEDIT Macro-bestand (Greenview Data) - Script/macrobestand voor de VEDIT-teksteditor (Greenview Data, Inc.); geschreven in de VDM-macrotaal om bewerkingstaken op tekst-, binaire of EBCDIC-bestanden te automatiseren. VEDIT is een niche maar nog steeds verkochte Windows/DOS-editor.
- Windows Defender Virusdefinitiemodule - Historisch gebruikt door Microsoft Windows Defender voor virusdefinitiemodules (.vdm-bestanden die bekende malware-handtekeningen bevatten); het moderne Defender gebruikt een ander updatemechanisme.
Programma's die VDM-bestanden openen
Windows4 apps
VDMTools
Betaald Open .vdm-bestanden voor typecontrole en bewijsvoering; verouderde tool, geef de voorkeur aan Overture.
VEDIT
Betaald Alleen voor VEDIT-macro .vdm-bestanden: open de VEDIT-teksteditor en voer macro's uit of bewerk ze.
Overture Tool
Open-source Project importeren → .vdm-bestanden toevoegen; typecontrole en animatie van specificaties via de Overture IDE.
VS Code (with Overture extension)
Open-source De Overture-gemeenschap biedt VS Code-taalondersteuning voor VDM; open .vdm voor syntaxismarkering. 
macOS2 apps
VDMTools
Free (academic) Open .vdm-bestanden voor typecontrole en bewijsvoering; verouderde tool, geef de voorkeur aan Overture.
Overture Tool
Open-source Project importeren → .vdm-bestanden toevoegen; typecontrole en animatie van specificaties via de Overture IDE. 
Linux2 apps
VDMTools
Free (academic) Open .vdm-bestanden voor typecontrole en bewijsvoering; verouderde tool, geef de voorkeur aan Overture.
Overture Tool
Open-source Project importeren → .vdm-bestanden toevoegen; typecontrole en animatie van specificaties via de Overture IDE. Technische details
diepe specificaties| Bestandscodering | Platte tekst - ASCII of UTF-8 |
| Dialecten | VDM-SL (modulair/plat), VDM++ (objectgeoriënteerd), VDM-RT (real-time/gedistribueerd) |
| ISO-standaard | ISO/IEC 13817-1:1996 (VDM-SL) |
| Syntaxisbasis | Verzamelingenleer, predicatenlogica, algebraïsche datatypen |
| Modulestructuur (VDM-SL) | `module`-trefwoord met secties voor `types`, `values`, `functions`, `operations` |
| Klassestructuur (VDM++) | `class`-trefwoord met instantievariabelen, methoden en invarianten |
| Typische bestandsgrootte | 1 KB - 200 KB |
| OS-ondersteuning | Windows, Linux, macOS - platformonafhankelijk tekstformaat |
| Primaire tooling | Overture Tool (op Eclipse gebaseerd, open source); VDMTools (commercieel, verouderd) |
| Alternatieve extensies | `.vdmsl` voor VDM-SL-bronnen, `.vdmpp` en `.vpp` voor VDM++-bronnen |
| Codegeneratie | Java- en C++-generatie vanuit VDM++/VDM-RT ondersteund door Overture Tool |
| Toepassingsdomeinen | Luchtvaart, medische apparatuur, financiële systemen, compilerontwerp, veiligheidskritische embedded systemen |
| Uitgebracht | 1970s (VDM-SL); ISO/IEC 13817-1 published 1996 |
| Laatste versie | VDM-SL (ISO/IEC 13817-1:1996); VDM++ (extension for OO, 2000s); VDM-RT (real-time extension) |
| Open standaard | Ja · royaltyvrij |
| Specificatie | www.overturetool.org |
VDM conversies
Community V&A
gevraagd door gebruikersNog geen vragen - wees de eerste om iets te vragen over VDM-bestanden.
