Was ist das VDM-Dateiformat?
.vdm ist ein Entwicklungsdateiformat zur Speicherung von Quellcode, der in den Spezifikationssprachen VDM-SL oder VDM++ geschrieben wurde. Eine .vdm-Datei ist reiner Text und kann mit jedem Texteditor bearbeitet werden. VDM-Dateien speichern formale Spezifikationen, die ein Modell eines Computersystems beschreiben. Die Verwendung von VDM-Spezifikationsdateien ermöglicht es Designern, eine übergeordnete Sicht auf das System zu erhalten - eine Sicht, die schwieriger zu erlangen ist, wenn man nur den Implementierungsquellcode liest. VDM-Dateien können auch als Basis für die Generierung von Codekomponenten dienen.
Vienna Development Method
Der VDM-Standard wurde in den 1970er Jahren im Wiener Labor von IBM entwickelt und ist eine der ältesten formalen Methoden für die Entwicklung von Computersystemen. VDM-SL wurde 1996 als ISO/IEC 13817-1 standardisiert. Es wurde weiterentwickelt, um objektorientierte Modellierung zu unterstützen, was zum VDM++-Standard führte, der ebenfalls .vdm-Dateien verwendet. Ein dritter Dialekt, VDM-RT, erweitert VDM++ für Echtzeit- und verteilte Systeme. Die Sprache wird in sicherheitskritischen Bereichen eingesetzt, darunter Betriebssystemdesign, Compiler, Avionik-Software und Steuerungssysteme für medizinische Geräte.
Das primäre Open-Source-Toolset ist das Overture Tool, eine Eclipse-basierte IDE, die aktiv von der Community gepflegt und in EU-Forschungs- und Industrieprojekten eingesetzt wird. Einige Tools verwenden die alternativen Dateiendungen .vdmsl und .vdmpp, um die beiden Hauptdialekte zu unterscheiden.
Sicherheit
RISIKO: LOWKlartext-Quellcodedateien; kein ausführbarer Inhalt. Kein bekannter Malware-Vektor.
Formatdetails
kurz gefasst- VEDIT Makro-Datei (Greenview Data) - Skript-/Makrodatei für den VEDIT-Texteditor (Greenview Data, Inc.); geschrieben in der VDM-Makrosprache zur Automatisierung von Bearbeitungsaufgaben an Text-, Binär- oder EBCDIC-Dateien. VEDIT ist ein Nischen-Editor für Windows/DOS, der immer noch vertrieben wird.
- Windows Defender Virendefinitionsmodul - Wurde historisch von Microsoft Windows Defender für Virendefinitionsmodule verwendet (.vdm-Dateien, die bekannte Malware-Signaturen enthalten); das moderne Defender verwendet einen anderen Aktualisierungsmechanismus.
Programme zum Öffnen von VDM-Dateien
Windows4 apps
VDMTools
Kostenpflichtig Öffnen von .vdm-Dateien für Typprüfung und Beweisführung; Legacy-Tool, Overture wird bevorzugt.
VEDIT
Kostenpflichtig Nur für VEDIT-Makro-.vdm-Dateien: VEDIT-Texteditor öffnen und Makros ausführen/bearbeiten.
Overture Tool
Open Source Projekt importieren → .vdm-Dateien hinzufügen; Typprüfung und Animation von Spezifikationen über die Overture-IDE.
VS Code (with Overture extension)
Open Source Die Overture-Community bietet VS Code-Sprachunterstützung für VDM; .vdm für Syntax-Highlighting öffnen. 
macOS2 apps
VDMTools
Free (academic) Öffnen von .vdm-Dateien für Typprüfung und Beweisführung; Legacy-Tool, Overture wird bevorzugt.
Overture Tool
Open Source Projekt importieren → .vdm-Dateien hinzufügen; Typprüfung und Animation von Spezifikationen über die Overture-IDE. 
Linux2 apps
VDMTools
Free (academic) Öffnen von .vdm-Dateien für Typprüfung und Beweisführung; Legacy-Tool, Overture wird bevorzugt.
Overture Tool
Open Source Projekt importieren → .vdm-Dateien hinzufügen; Typprüfung und Animation von Spezifikationen über die Overture-IDE. Technische Details
technische Spezifikation| Dateikodierung | Klartext - ASCII oder UTF-8 |
| Dialekte | VDM-SL (modular/flach), VDM++ (objektorientiert), VDM-RT (Echtzeit/verteilt) |
| ISO-Standard | ISO/IEC 13817-1:1996 (VDM-SL) |
| Syntax-Basis | Mengenlehre, Prädikatenlogik, algebraische Datentypen |
| Modulstruktur (VDM-SL) | `module`-Schlüsselwort mit den Abschnitten `types`, `values`, `functions`, `operations` |
| Klassenstruktur (VDM++) | `class`-Schlüsselwort mit Instanzvariablen, Methoden und Invarianten |
| Typische Dateigröße | 1 KB - 200 KB |
| Betriebssystem-Unterstützung | Windows, Linux, macOS - plattformunabhängiges Textformat |
| Primäre Werkzeuge | Overture Tool (Eclipse-basiert, Open Source); VDMTools (kommerziell, Legacy) |
| Alternative Dateiendungen | `.vdmsl` für VDM-SL-Quellen, `.vdmpp` und `.vpp` für VDM++-Quellen |
| Codegenerierung | Java- und C++-Generierung aus VDM++/VDM-RT wird vom Overture Tool unterstützt |
| Anwendungsbereiche | Avionik, medizinische Geräte, Finanzsysteme, Compiler-Design, sicherheitskritische eingebettete Systeme |
| Veröffentlicht | 1970s (VDM-SL); ISO/IEC 13817-1 published 1996 |
| Neueste Version | VDM-SL (ISO/IEC 13817-1:1996); VDM++ (extension for OO, 2000s); VDM-RT (real-time extension) |
| Offener Standard | Ja · lizenzgebührenfrei |
| Spezifikation | www.overturetool.org |
VDM-Konvertierungen
Community Q&A
von Nutzern gefragtNoch keine Fragen - stellen Sie die erste Frage zu VDM-Dateien.
