Verifying common object-oriented design-patterns in stateful actor-languages

• Applicant: Professor Dr.-Ing. Steffen Helke
• Subject Area: Software Engineering and Programming Languages
• Term: from 2010 to 2016
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 170470060

Moderne Computer verfügen heute über mehrere, parallele Prozessierungseinheiten, deren Leistungsreserven dediziert erschlossen werden müssen. Threads und Locks sind als Programmierabstraktion schwer überschaubar, fehleranfällig und zur Programmierung vieler paralleler Einheiten nicht geeignet. Um nebenläufige Softwaresysteme auf breiter Basis entwickeln zu können, bedarf es einfacherer Ausdrucksmittel und verlässlicher Entwurfspraktiken. Eine einfache und vielversprechende Abstraktion für parallele Programmabschnitte sind nebenläufige Objekte bzw. Actors. Aufbauend auf den heutigen objektorientierten Programmierpraktiken und gemäß der Idee »everything is an actor« besitzt die Actor-Programmierabstraktion das Potential, die Leistungsreserven paralleler Systeme auf breiter (Entwickler-)Basis zu erschließen. In dem vorgeschlagenen Projekt werden etablierte objektorientierte Entwurfspraktiken in Form von Design-Patterns aus dem sequentiellen objektorientierten Kontext in einen nebenläufigen Actor-Objekt-Kontext übertragen und dort hinsichtlich ihrer semantischen Stabilität und Wiederverwendbarkeit untersucht. Das Projekt befasst sich inhaltlich (1) mit der formalen Spezifikation von Design-Patterns, (2) mit der beweisorientierten Mechanisierung von Actor-Objekt-Logiken und (3) mit der Verifikation sicherheitskritischer Design-Pattern-Eigenschaften im nebenläufigen Kontext. Das Projekt soll insgesamt etablierte Entwurfspraktiken des Software- Engineering in die Domäne paralleler Systeme überführen und ihnen außerdem eine präzise formale Fundierung geben.

• DFG Programme: Research Grants
• Participating Person: Professor Dr.-Ing. Stefan Jähnichen