Es gibt Eigenschaften, die kein Testlauf zeigen kann. Dass ein Regler unter allen zulässigen Anfangswerten stabil bleibt, dass ein numerisches Verfahren seine Fehlerschranke einhält, dass eine Implementierung ihre Spezifikation erfüllt: Testen prüft Stichproben, ein Beweis prüft alle Fälle. Dieser Workshop zeigt an einem eigenen Beispiel, wie ein maschinengeprüfter Beweis entsteht, was er kostet und wo seine Grenzen liegen.
Der rote Faden ist eine Aussage, die Ihr Team aus der eigenen Arbeit kennt: eine Stabilitätsaussage, eine Fehlerschranke, eine Invariante. Im Workshop wird sie formal aufgeschrieben, im Beweisassistenten bewiesen und in ein ausführbares Programm überführt. Jeder Schritt findet am selben Beispiel statt, so bleibt der Zusammenhang zwischen Spezifikation, Beweis und Code sichtbar.
Der Workshop richtet sich an Regelungstechnik-, Safety- und Embedded-Teams, die Eigenschaften absichern müssen, für die Tests nicht ausreichen, sowie an Forschungsgruppen und Entwicklungsabteilungen, die ein Verifikationsvorhaben planen oder einen Förderantrag vorbereiten. Vorausgesetzt werden Programmiererfahrung und Sicherheit in Analysis auf Ingenieurniveau. Vorerfahrung mit Beweisassistenten ist nicht nötig.
Was der Workshop nicht leistet: Er liefert keinen Normnachweis. Formale Verifikation kann Argumente für eine Sicherheitsargumentation beisteuern, ersetzt aber keine Zulassung und keine Abnahme. Er liefert auch keine verifizierte Codebasis in zwei Tagen, realistisch ist eine abgegrenzte Eigenschaft an einer abgegrenzten Komponente. Und er ersetzt keine Tests: Der Beweis gilt für Modell und Spezifikation, ob das Modell die Anlage trifft, klären weiterhin Messung und Test. Aussagen über Rocq und Lean stützen sich auf geprüfte Bibliotheks- und Literaturstände, nicht auf eigene Projektlaufzeiten.
Alle Formate: Deutsch & Englisch.
Alle Preise verstehen sich netto zzgl. gesetzlicher Umsatzsteuer. Das Angebot richtet sich ausschließlich an Unternehmer im Sinne des § 14 BGB.
Dr.-Ing. Grigory Devadze. Formale Verifikation ist mein eigenes Forschungsfeld, nicht ein Kapitel aus einem Lehrbuch.
Schulungen & Projekte u. a. für Siemens AG und SRH Hochschule Berlin.
→ Profil und Referenzen ansehen
Ja. Grundlagen, Spezifikationsarbeit und Extraktionsdenken sind übertragbar, und der Werkzeugvergleich ist Teil des Programms. Die tiefste eigene Praxiserfahrung liegt beim Minlog-Zweig, das sage ich offen, statt Erfahrung zu behaupten, die ich nicht habe.
Nein. Nötig ist Sicherheit in der Analysis auf Ingenieurniveau und die Bereitschaft, Aussagen präzise aufzuschreiben. Das ist der eigentliche Umstellungsaufwand.
Nicht in einem Sprint. Sinnvoll ist der Einstieg dort, wo ein Fehler teuer oder gefährlich ist und die Eigenschaft klar umrissen werden kann. Der Orientierungsworkshop beantwortet genau diese Frage für Ihren Fall.
Aus konstruktiv geführten Beweisen lässt sich Code extrahieren, und im Workshop tun wir das. Ob dieser Code produktiv eingesetzt wird, ist eine eigene Entscheidung mit eigenen Anforderungen an Schnittstellen und Laufzeit.
Ja, das ist das Format „Begleitung im Vorhaben“. Erfahrung mit Antragstellung und Durchführung geförderter Vorhaben liegt vor.
Weitere eigene Forschung: Research-Case Predictive Analytics in der Landwirtschaft
Kurzes Vorgespräch zu Ihrer Eigenschaft und Ihrem Stack, danach ein konkretes Angebot mit Workshop-Agenda.
Dr.-Ing. Grigory