Heutige Hardware- und Softwaresysteme werden zunehmend komplexer und umfangreicher. Zusätzliche sicherheitskritische Anforderungen, die mitunter auch Menschenleben schützen sollen, sind nicht selten. Um Fehler bei der Fertigung dieser Systeme schon möglichst in einem frühen Stadium der Entwicklung zu vermeiden, sind Verifikationsmethoden während der Modellierungs- und Spezifikationsphase wünschenswert. Da Anforderungen aber derzeit überwiegend natürlichsprachlich vorliegen, sind Verifikationen oft mühsam und zeitaufwendig. Dennoch gibt es Möglichkeiten, den informellen Schein der natürlichen Sprache beizubehalten und Verifikationen sogar automatisiert durchlaufen zu lassen. Das Ziel dieser Masterarbeit ist die Fertigstellung eines Prozesses, der es erlaubt, Systeme visuell zu modellieren, geeignet informell zu spezifizieren und anschließend automatisiert zu verifizieren. Die Grundlagen bieten auf der einen Seite die Systembeschreibungssprache SysML und eine für die vertragsbasierte Spezifikation geeignete semiformale Templatesprache. Auf der anderen Seite können formal definierte Systeme mit dem Befehlszeilenwerkzeug OCRA bereits auf Korrektheit geprüft werden. Um diese Lücke zu schließen werden Regeln definiert, welche die semiformale Templatesprache schrittweise in eine lineare temporale Logik für hybride Systeme übersetzt. Diese Übersetzungen werden in einen vorhandenen Prototypen integriert, der die zuvor modellierten und informell spezifizierten Systeme automatisert in die OCRA verständliche Sprache überführt. Mit Hilfe eines zusätzlich entwickelten Plugins werden die Ergebnisse der Korrektheitsprüfung anschaulich visualisiert. Abschließend wird der vollständige Prozess anhand zweier Fallbeispiele validiert.