Automatisierte Synthese von Programmausdrücken (AutoSynth)

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

In diesem Forschungsvorhaben sollen Verfahren zur automatischen Synthese von Programmausdrücken entwickelt werden, um eine neue Art des Systementwurfs zu etablieren. Dabei ist vorgesehen, dass der Entwickler ein „Programmskelett“ des späteren Programms erstellt, welches zwar bereits alle Anweisungen des Programms enthält, aber dabei manche Ausdrücke in den Anweisungen als Syntheseziele offen lässt. Unter Beachtung zusätzlich gegebener Spezifikationen ermitteln dann die in diesem Forschungsvorhaben geplanten Verfahren hierfür geeignete Programmausdrücke, so dass das somit entstandene vollständige Programm die gegebenen Spezifikationen erfüllt. Die Untersuchungen dieses Projekts umfassen dabei die syntaktische Repräsentation des Suchraums für diese Programmausdrücke, die Anpassung bekannter Verfahren der Controller-Synthese bzw. der Spieltheorie, den Einsatz abstrakter Interpretation sowie aktueller Deduktionsverfahren wie Unifikation und SMT-Verfahren zur Behandlung höherer Datentypen. Dabei soll mit einfachen Sicherheitseigenschaften begonnen werden, die dann in späteren Phasen des Projekts auf ω-reguläre Eigenschaften erweitert werden, so dass gängige Spezifikationen reaktiver Systeme behandelt werden können.