 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||
| |||||||||||||||||||||
| |||||||||||||||||||||
|
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Vergleich von Model Checking mit ATP |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Grundsätzlich können automatische Beweiser und Model Checker ohne Kenntnis der zugrundeliegenden Formalismen eingesetzt werden. Das ihr großer Vorteil im Vergleich zu nicht automatischen Verfahren, z.B. interaktiven Theorem Beweisern, bei denen man Kenntnis des zugrundeliegenden Kalküls besitzen muss.
Hinsichtlich der Mächtigkeit der beiden Methoden hängt viel von dem Anwendungsszenerio des automatischen Verifikationswerkzeuges ab, in der Form, dass entweder Optimierungen im Zustandsraum existieren für den Model Checker bzw. "Beweisabkürzungen" für den automatischen Beweiser. Aktuell wurden viele Optimierungen im Bereich Model Checking entwickelt, daher existieren bereits zahlreiche praktische Anwendungskontexte, in denen Model Checking erfolgreich eingesetzt wurde und wird. Obwohl automatische Beweiser bereits seit den 50er Jahren existieren, ist deren komfortabler Einsatz (z.B. ohne Kenntnis der Kalküle von einer weiteren, im Entwicklungsprozess genutzten Notation) oftmals nicht möglich, da die Beweiser i.d.R. nur ihre spezielle Notation (z.B. Teilmenge der Prädikatenlogik) unterstützten, was den Einsatz in der Industrie oftmals unnötig erschwert. Beide Techniken haben ihre Vorteile, abhängig vom Anwendungsbereich und für die Entscheidung, welche eingesetzt werden soll ist es notwendig, diesen genauestens zu untersuchen. Zurück zum Überblick Automatisches Beweisen im Bereich der Softwareentwicklung Nächster Gliederungspunkt Mögliche Anwendungen von Automatischen Beweisen | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Vergleich von Model... | ||||
| ||||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
