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

• Applicant: Professorin Dr. Heike Wehrheim
• Subject Area: Computer Architecture, Embedded and Massively Parallel Systems
• Term: from 1999 to 2002
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5207456

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.

• DFG Programme: Research Fellowships