Verifikationstechniken für Spezifikationen verteilter Systeme mit objektorientierten daten- und prozeßorientierten Verhaltensbeschreibungen

点击翻译按钮获取中文摘要

Die Integration von objekt-orientierten Daten- und prozeßorientierten Verhaltensbeschreibungen ist die Basis vieler moderner Softwaremodellierungssprachen. In der geplanten Arbeit sollen Verifikationstechniken für den Korrektheitsnachweis solcherart modellierter verteilter, kommunizierender Systeme entwickelt werden. Wichtigster Aspekt der Techniken ist die Bewältigung der Komplexität des zu verifizierenden Systems, die bei verteilten Softwaresystemen insbesondere durch das kombinierte Auftreten von großen Datenmengen und hoher Nebenläufigkeit der Komponenten entsteht. Basis für die Verifikation eines Softwareentwurfs ist eine formale Semantik der benutzten Modellierungssprache. In der geplanten Arbeit soll die formale Methode CSP-OZ als semantische Basis für Daten- und Verhalten- integrierende Modellierungssprachen benutzt werden. CSP-OZ ist eine Kombination der zustandsorientierten Methode Object-Z und der Prozeßalgebra CSP und besitzt eine einheitliche Semantik für beide Beschreibungsteile. Ziel des Vorhabens ist die Entwicklung von Verifikationstechniken für CSP-OZ-Spezifikationen unter Ausnutzung der objekt-orientierten Strukturierung.