Projekt R1, Zusammenfassung

Das Projekt R1 erforscht die automatische Verifikation von Realzeitsystemen, die durch Spezifikationen mit den drei Dimensionen Prozessverhalten, komplexen unendlichen Datenstrukturen und kontinuierlicher Zeit beschrieben werden. Dazu werden Transformations- und Dekompositionstechniken mit Beweisverfahren verknüpft, die auf den Paradigmen der Abstraktionsverfeinerung und der lokalen Theorieerweiterung beruhen.