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

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

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.