Die Ausdruckskraft von Abstract State Machines

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

Abstract State Machines (ASMs) wurden von Yuri Gurevich schon Mitte der 80 er Jahre als ein neues Systemmodell vorgeschlagen, das im Vergleich zu herkömmlichen System- modellen eine natürlichere und intuitivere formale Beschreibung von Algorithmen erlaubt. Dies gelingt, indem die Zustände und Schritte eines Algorithmus mittels beliebig gewählter Objekte und Operationen beschrieben werden. ASMs werden seither erfolgreich als modellbasierte Entwurfs- und Analysetechnik für komplexe industrielle Systeme eingesetzt. Aufgrund der vielffältigen Anforderungen aus der Praxis wurden mehrere Varianten von ASMs entwickelt, die sich in ihrer Ausdruckskraft unterscheiden. Im Jahr 2000 gelang Gurevich eine erstaunlich elegante formale Charakterisierung der Ausdrucksstärke sequentieller ASMs. Später haben Blass und Gurevich auch parallele und interaktive ASMs charakterisiert. Im Rahmen dieses Projektes ist es uns gelungen, die Ausdrucksstärke verteilter und nichtdeterministischer ASMs intuitiv und einfach verständlich zu charakterisieren. In der hier beantragten Fortsetzung des Projektes möchten wir in entsprechender Weise die Ausdrucksstärke parallel-nichtdeterministischer ASMs charakterisieren, welche für den ASM-basierten Systementwurf eine besonders wichtige Rolle spielen. Zudem möchten wir dieses Projekt abschliessen, indem wir die bisher isolierten Charakterisierungen von ASMs in eine einheitliche Begriffswelt einordnen und miteinander vergleichen.