Hier werden die Unterschiede zwischen zwei Versionen gezeigt.
|
lehre:abschlussarbeiten:sb:modulareboolescheabstraktion [2012/05/24 10:23] biallas |
lehre:abschlussarbeiten:sb:modulareboolescheabstraktion [2012/05/24 10:23] (aktuell) biallas |
||
|---|---|---|---|
| Zeile 8: | Zeile 8: | ||
| ===== Vorgehensweise ===== | ===== Vorgehensweise ===== | ||
| - | Ausgangspunkt ist die Zwischensprache. Es wird anhand einer statischen Analyse festgestellt, wo es durch eine Auswertung einer Funktion oder einer Berechnung mit mehreren Variablen zu einer Zustandsexplosion kommen kann. Für solche Stellen wird eine neue Boolesche Eingabevariable erzeugt und der problematische Ausdruck durch diese ersetzt. Beim Model-Checking kann es nun sein, dass ein Gegenbeispiel zu einer Formel gefunden wird. Aufgrund der Überapproximation, die aus der Ersetzung des Ausdrucks resultiert, muss nun geprüft werden, ob das Gegenbeispiel realisierbar ist oder nur aus der Überapproximation resultiert. Dazu wird der ursprüngliche Ausdruck analysiert und falls nötig wieder eingefügt. Die Implementierung wird mit verschiedenen SPS-Programmen getestet | + | Ausgangspunkt ist die Zwischensprache. Es wird anhand einer statischen Analyse festgestellt, wo es durch eine Auswertung einer Funktion oder einer Berechnung mit mehreren Variablen zu einer Zustandsexplosion kommen kann. Für solche Stellen wird eine neue Boolesche Eingabevariable erzeugt und der problematische Ausdruck durch diese ersetzt. Beim Model-Checking kann es nun sein, dass ein Gegenbeispiel zu einer Formel gefunden wird. Aufgrund der Überapproximation, die aus der Ersetzung des Ausdrucks resultiert, muss nun geprüft werden, ob das Gegenbeispiel realisierbar ist oder nur aus der Überapproximation resultiert. Dazu wird der ursprüngliche Ausdruck analysiert und falls nötig wieder eingefügt. Die Implementierung wird mit verschiedenen SPS-Programmen getestet. |
| + | |||
| + | ===== Ansprechpartner ===== | ||
| + | |||
| + | * [[:lehrstuhl:mitarbeiter:biallas]] | ||