 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||
| |||||||||||||||||||||
| |||||||||||||||||||||
|
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Automatisches Beweisen im Bereich der Softwareentwicklung |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
Automatisches Beweisen (engl. Automated Theorem Proving) ist eine Technik zur vollständigen, automatischen Verifikation. Das Forschungsgebiet des Automatischen Beweisens ist bereits relativ alt. Mitte der 50er Jahre wurden erste Automatische Beweiser entwickelt. Die Grundlage bildete zunächst die sog.  Presburger Arithmetik, welche eine Einschränkung der Prädikaten-Logik erster Ordnung darstellt, die entscheidbar ist. Mittlerweile gibt es Automatische Beweiser auch für die Prädikatenlogik erster Ordnung mit Gleichheit und einige modale Logiken (sofern Transformationen zur Prädikaten-Logik erster Ordnung existieren). Automatisches Beweisen bietet neben Model Checking eine Möglichkeit Programme und Hardware automatisch vollständig zu verifizieren.
In den folgenden Bausteinen werden allgemeine Anforderungen an die Verifikation aus dem Bereich Software Engineering identifiziert, Interaktive Beweiser und Automatische Beweiser erläutert und in Bezug auf die identifizierten Anforderungen untersucht. Ein Werkzeugbaustein widmet sich dem Automatischen Beweiser DARWIN. Die zwei Bausteine Beispiel1, Beispiel2 thematisieren Anwendungsbeispiele, in denen Automatisches Beweisen exemplarisch zum Einsatz kommt. Weiterhin werden die Werkzeuge KeY, welches eine Integration eines Automatischen Beweisers in ein CASE Tool zur UML gestützen Entwicklung von Software darstellt und zum anderen Amphion, ein Projekt der NASA zur Softwarewiederverwendung vorgestellt. Gemeinsamkeiten und Unterschiede von Model Checking und Automatisches Beweisen werden anschließend betrachtet. Abschließend wird eine mögliche Entwicklung des Automatischen Beweisens in der Zukunft diskutiert und ein Fazit gezogen. | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren
| ||||||||||||||
|
