Deduktive Modellierung von Java

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

In den vergangenen zwei Förderungsperioden des Bali-Projekts ist es gelungen, die wichtigsten Aspekte der Programmiersprache Java und der dazugehörigen Ablaufumgebung im Theorembeweiser Isabelle/HOL zu modellieren und verifizieren: Quellsprache Java inklusive einer Hoare-Logik, Zielsprache JVM, Übersetzer, Bytecode Verifier und die dazugehörigen Korrektheitsbeweise. Primäres Ziel dieses Verlängerungsantrags ist die Integration der bisher erfolgten Arbeiten zu einem einheitlichen Ganzen: einer automatisch aus dem formalen Modell generierten Ablaufumgebung für die von uns betrachtete Teilsprache von Java, als formales Gegenstück zu Suns Übersetzer und Ausführungsumgebung. Dies integrierte Modell soll dann auf ein Problem bei Java Chipkarten angewandt werden: der Verifikation eines zeit- und platzeffizienten Bytecode Verifiers, der auch auf Chipkarten paßt. Ferner soll das Modell um zwei Punkte erweitert werden, die die Tür für weitere wissenschaftliche und praktische Arbeiten öffnen: Behandlung von Parallelismus, insbesondere bei der Programmverifikation, und der Schritt von der Programmierung zur Systementwicklung durch die Hinzunahme von Teilen der UML.