Projekt RAP & TIP

Formale Spezifikationen sind Problembeschreibungen, die für Menschen leichter verständlich sind als maschinen-orientierte Darstellungen. Da solche Beschreibungen stark an Konzepte aus den Bereichen Mathematik und Logik angelehnt sind, haben sie einen sehr hohen Abstraktionsgrad.

Das RAP System ist eine Arbeitsumgebung für das schnelle Erstellen und Austesten von formalen Spezifikationen (Stichwort: rapid prototyping). Im Rahmen des FORWISS Projekts RAP & TIP wird für das RAP System eine benutzerfreundliche Bedienoberfläche entwickelt (Standard X-Window-System). Außerdem werden mehrere Verbesserungen bezüglich des Laufzeitverhaltens und Erweiterungen der Mächtigkeit des Systems durchgeführt. Das alles soll helfen, die Akzeptanz des Systems steigern.

Das TIP System ist ein induktiver Theorembeweiser. Die bearbeitbaren Spezifikationen stimmen mit denen des RAP Systems überein. Dadurch ergänzen sich die beiden Systeme sehr gut. Mit Hilfe des TIP Systems kann man die Gültigkeit von Theoremen (Aussagen bezüglich formaler Spezifikationen) beweisen. Im Rahmen des RAP & TIP Projekts wird der zentrale Beweisalgorithmus verändert und erweitert. Schwerpunkt sind dabei die Erweiterungen von TIP für den Umgang mit bedingten Theoremen. Dies ist ein sehr wichtiger Schritt für die Verifikation von Software. Außerdem sollen neuere Forschungsergebnisse auf dem Gebiet der Theorembeweiser in das TIP System einfließen.