 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||
| |||||||||||||||||||||
| |||||||||||||||||||||
|
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Anforderungen an Verifikationstechniken |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Eine Verifikationstechnik, die in der Softwareentwicklung eingesetzt werden soll, muss bestimmte Anforderungen erfüllen.
1. Es ist wichtig, dass ein zu überprüfender Ausdruck innerhalb einer "akzeptablen" Zeit ausgewertet wird. Die akzeptable Zeit hängt hierbei von der Art der Anwendung ab. Gibt es beispielsweise einen Benutzer, der ohne die Antwort nicht weiterarbeiten kann, oder muss eine Entscheidung schnell gefällt werden, weil sonst eine sicherheitskritische Situation entsteht. 2. Weiterhin sollte jede, im entsprechenden Anwendungskontext auftretende, Eigenschaft, die verifiziert werden soll, auch ausdrückbar in der Logik sein. Das heißt die Ausdrucksstärke des Automatischen Beweisers muss entsprechend groß sein. 3. Auch die Verlässlichkeit der Antwort ist entscheidend. "Kann ich der Antwort trauen?" 4. Für manche Anwendungen ist es notwendig, dass ein Mensch in der Lage ist die Ausgabe des Programms zu lesen. Beispielsweise kann es nötig sein um die Verlässlichkeit der Antwort zu überprüfen. 5. Interessant ist auch die Frage, ob das System erweitert werden kann auf andere Logiken. Diese Anforderungen werden nun für die einzelnen Verifikationsmethoden (interaktive Beweiser und automatische Beweiser) näher betrachtet. Zurück zum Überblick: Automatisches Beweisen im Bereich der Softwareentwicklung Nächster Gliederungspunkt: Interaktive Beweiser | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Anforderungen an Verifikationstechniken | ||||
| ||||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
