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).
Seminar und Anbieter vergleichen
Öffentliche Schulung
Diese Seminarform ist auch als Präsenzseminar bekannt und bedeutet, dass Sie in unseren Räumlichkeiten von einem Trainer vor Ort geschult werden. Jeder Teilnehmer hat einen Arbeitsplatz mit virtueller Schulungsumgebung. Öffentliche Seminare werden in deutscher Sprache durchgeführt, die Unterlagen sind teilweise in Englisch.
Inhausschulung
Diese Seminarform bietet sich für Unternehmen an, welche gleiche mehrere Teilnehmer gleichzeitig schulen möchten. Der Trainer kommt zu Ihnen ins Haus und unterrichtet in Ihren Räumlichkeiten. Diese Seminare können in Deutsch - bei Firmenseminaren ist auch Englisch möglich gebucht werden.
Webinar
Diese Art der Schulung ist geeignet, wenn Sie die Präsenz eines Trainers nicht benötigen, nicht Reisen können und über das Internet an einer Schulung teilnehmen möchten.
Fachbereichsleiter / Leiter der Trainer / Ihre Ansprechpartner
-
Michael Adler
Telefon: + 41 (800) 225127
E-Mail: michael.adler@seminar-experts.ch -
Stefano Conti
Telefon: + 41 (800) 225127
E-Mail: stefano.conti@seminar-experts.ch
Seminardetails
| Dauer: | 3 Tage ca. 6 h/Tag, Beginn 1. Tag: 10:00 Uhr, weitere Tage 09:00 Uhr |
| Preis: |
Öffentlich und Webinar: CHF 1.797 zzgl. MwSt. Inhaus: CHF 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: | Basel, Bern, Luzern, Sankt Gallen, Winterthur, Zürich |
| 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 +41 (800) 225127 |
Seminartermine
Die Ergebnissliste kann durch Anklicken der Überschrift neu sortiert werden.
