COPY - Spezifikation und Verifikation objekt-orientierter Design-Patterns im Kontext nebenläufiger Objektsemantiken

Um nebenläufige Softwaresysteme auf breiter Basis entwickeln zu können, bedarf es einfacher Ausdrucksmittel und verlässlicher Entwurfspraktiken. Eine einfache und vielversprechende Abstraktion für parallele Programmierabschnitte sind nebenläufige Objekte bzw. Actors.

Im COPY-Projekt werden etablierte objektorientierte Entwurfspraktiken in Form von DesignPatterns aus dem sequentiellen objektorientierten Kontext in einen nebenläufigen Actor-Object-Kontext übertragen und dort hinsichtlich ihrer semantischen Stabilität und Wiederverwendbarkeit untersucht. Das Projekt befasst sich inhaltlich

• mit der formalen Spezifikation von DesignPatterns,
• mit der beweisorientierten Mechanisierung von Actor-Object-Logiken und
• mit der Verifikation sicherheitskritischer Design-Pattern-Eigenschaften im nebenläufigen Kontext.

Das Projekt soll etablierte Entwurfspraktiken des Software-Engineering in die Domäne paralleler Systeme überführen und ihnen außerdem eine präzise formale Fundierung geben.