 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||
| |||||||||||||||||||||
| |||||||||||||||||||||
|
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Automatisches Beweisen (Fazit) |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Automatisches Beweisen ist bereits ein, für die Informatik gesehen, sehr altes Forschungsgebiet. Trotz alledem hat es sich in der Wirtschaft bislang nicht etablieren können, da die Verlässlichkeit der Beweise nicht verifiziert werden kann und der Overhead durch die Anwendung formaler Methoden in der Softwareentwicklung oft gefürchtet wird. Einige Projekte haben jedoch in den letzten Jahren gezeigt, dass gerade durch den Einsatz formaler Methoden die Produktivität deutlich erhöht werden kann. So ist Wiederverwendung von Softwarefragmenten viel einfacher möglich, wenn deren Spezifikation formal vorliegt. Das Amphion Projekt zeigt, dass sogar automatische Wiederverwendung von Software möglich ist. Auch die Einbettung in den täglichen Alltag eines Software Entwicklers ist durchaus möglich. So gibt es mit KeY beispielsweise eine Einbettung von Automatischem Beweisen in ein kommerzielles CASE-Tool. Der Vergleich mit Model Checking hat gezeigt, dass die beiden Techniken unterschiedliche Anwendungsbereiche haben. Zwar gibt es Überschneidungen, jedoch haben beide ihre speziellen Vorzüge. Daher mag es sein, dass in bestimmten Bereichen in denen z.Z. noch Model Checking eingesetzt wird in Zukunft Automatisches Beweisen eine Anwendung findet. Auch die Kombination der beiden Techniken ist durchaus denkbar. Alles in allem wird die Bedeutung von Automatischem Beweisen in den nächsten Jahren sicher zunehmen, da durch die Weiterentwicklung der Theorien die Performance stark gesteigert wird und durch den immer größeren bedarf, Software zu verifizieren und wiederzuverwenden die Notwendigkeit formale Methoden in der Softwareentwicklung einzusetzen deutlich steigen wird. Die Hardwareindustrie hat spätestens seit der Auslieferung des Pentium 60 begriffen, dass es nötig ist Produkte zu verifizieren und auch in der Softwareindustrie wächst das Verständnis für diese Methoden.
Zurück zum Überblick Automatisches Beweisen im Bereich der Softwareentwicklung | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Automatisches Beweisen... | ||||
| ||||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
