Kontinuierliche Assurance: Formalverifikation & Assurance‑Cases für autonome Systeme

Autonome Systeme müssen ihr Vertrauen in Korrektheit und Sicherheit über den gesamten Lebenszyklus hinweg – von der Konzeption über die Inbetriebnahme bis hin zur Weiterentwicklung – kontinuierlich nachweisen können. Traditionelle Ansätze trennen Entwicklungs‑ und Laufzeit‑Sicherheitsnachweise, was zu fragmentierten Argumenten führt, die sich nicht an Änderungen im Betrieb anpassen lassen.

Um dieses Problem zu lösen, stellen die Autoren ein einheitliches Continuous Assurance Framework vor, das Design‑, Laufzeit‑ und Evolutions‑Sicherheitsnachweise in einen nachvollziehbaren, modellgesteuerten Workflow integriert. Im Design‑Zeit‑Modul werden zwei formale Verifikationsmethoden eingesetzt: RoboChart zur funktionalen Korrektheitsprüfung und PRISM zur probabilistischen Risikoanalyse.

Ein weiteres Highlight ist die modellbasierte Transformationspipeline, die als Eclipse‑Plugin implementiert ist. Sie regeneriert automatisch strukturierte Assurance‑Argumente, sobald sich formale Spezifikationen oder deren Verifikationsergebnisse ändern, und gewährleistet damit eine lückenlose Rückverfolgbarkeit.

Die Vorgehensweise wird anhand eines Szenarios mit einem Kernkraftwerks‑Inspektionsroboter demonstriert. Dabei wird gezeigt, wie das Framework die Trilateral AI Principles unterstützt und regulatorisch empfohlene Best Practices umsetzt.