SPARK Grundlagen: Contracts, GNATprove, Flow Analysis, Proof Workflow
Agenda (Tag 1–3)
- SPARK Überblick: Ziele, Subset, Nachweisarten
- Tool-Workflow: Analyse, Proof, Reports
- Übung: Erste verifizierbare Funktion mit Pre/Post
- Contracts vertiefen: Invariants, Typen als Spezifikation
- Flow Analysis: Datenflüsse, Initialisierung, Side Effects
- Übung: Komponente mit sauberem Datenfluss
- Proof-Workflow: typische Findings, Ursachen, Fixes
- Modularisierung für Proof: Schnittstellen, Hilfsfunktionen, Lemmas (Einführung)
- Abschluss-Lab: Mini-Komponente end-to-end verifizieren
Step-by-step-Praxispfad
- SPARK-fähigen Codebereich definieren (klarer Scope, keine unnötigen Abhängigkeiten).
- Kernfunktion implementieren und erste Analyse ausführen.
- Precondition ergänzen (Eingabebereiche, Typgrenzen).
- Postcondition definieren (fachliche Zusicherung messbar formulieren).
- Flow Analysis Findings beheben (Initialisierung, Abhängigkeiten, Nebenwirkungen).
- Proof iterieren (kleine Schritte, Reports systematisch nutzen).
- Review: Vertrag vs. Anforderung (Lesbarkeit und Wartbarkeit der Spezifikation).
Fachbereichsleiter / Leiter der Trainer / Ihre Ansprechpartner
-
Lucas Beich
Telefon: + 49 (221) 74740055
E-Mail: lucas.beich@seminar-experts.de -
Paul Goldschmidt
Telefon: + 49 (221) 74740055
E-Mail: paul.goldschmidt@seminar-experts.de
Seminardetails
| Dauer: | 3 Tage ca. 6 h/Tag, Beginn 1. Tag: 10:00 Uhr, weitere Tage 09:00 Uhr |
| Preis: |
Öffentlich oder Live Stream: € 1.797 zzgl. MwSt. Inhaus: € 5.100 zzgl. MwSt. |
| Teilnehmeranzahl: | min. 2 - max. 8 |
| Teilnehmer: | Safety-/Security-Teams, Entwicklung, Qualitätsmanagement, Verifikationsrollen |
| Voraussetzungen: | Ada Grundlagen (A01). A02 ist hilfreich, aber nicht zwingend |
| Standorte: | Stream Live, Inhaus/Firmenseminar, Berlin, Bremen, Darmstadt, Dresden, Erfurt, Essen, Flensburg, Frankfurt, Freiburg, Friedrichshafen, Hamburg, Hamm, Hannover, Jena, Kassel, Köln, Konstanz, Leipzig, Luxemburg, Magdeburg, Mainz, München, Münster, Nürnberg, Paderborn, Potsdam, Regensburg, Rostock, Stuttgart, Trier, Ulm, Wuppertal, Würzburg |
| Methoden: | Vortrag, Demonstrationen, praktische Übungen am System |
| Seminararten: | Öffentlich, Webinar, Inhaus, Workshop - Alle Seminare mit Trainer vor Ort, Webinar nur wenn ausdrücklich gewünscht |
| Durchführungsgarantie: | ja, ab 2 Teilnehmern |
| Sprache: | Deutsch - bei Firmenseminaren ist auch Englisch möglich |
| Seminarunterlage: | Dokumentation auf Datenträger oder als Download |
| Teilnahmezertifikat: | ja, selbstverständlich |
| Verpflegung: | Kalt- / Warmgetränke, Mittagessen (wahlweise vegetarisch) |
| Support: | 3 Anrufe im Seminarpreis enthalten |
| Barrierefreier Zugang: | an den meisten Standorten verfügbar |
| Weitere Informationen unter + 49 (221) 74740055 |
Seminartermine
Die Ergebnissliste kann durch Anklicken der Überschrift neu sortiert werden.
