316
5 Bewertung und Validierung
Definition 5.43: Die Ausführung eines Modells eines Systems, in dem keine Komponente durch eine computerbasierte Simulation realisiert wird, heißt Rapid Prototyping. Dabei werden alle Bestandteile durch realistische Komponenten dargestellt.
Einige dieser Komponenten sollten nicht die endgültig verwendeten Komponenten
sein, da das System ansonsten dem realen System entspräche.
In vielen Fällen sollten Entwürfe in realistischen Umgebungen getestet werden, bevor
die endgültige Version produziert wird. Steuergeräte von Autos sind ein hervorragendes Beispiel hierfür. Diese Systeme sollten von Testfahrern in verschiedenen
Umgebungen verwendet werden, bevor sie in die Massenproduktion gehen. Daher
entwirft die Automobilindustrie Prototypen. Diese Prototypen sollten sich größtenteils wie die endgültigen Systeme verhalten, sie können dabei aber schwerer sein,
mehr Energie verbrauchen oder andere Eigenschaften besitzen, die einen Testfahrer
nicht stören. Der Begriff „Prototyp” kann für das gesamte System aus elektrischen
und mechanischen Komponenten verwendet werden. Die Unterscheidung zwischen
Rapid Prototyping und Emulation beginnt aber unscharf zu werden. Rapid Prototyping selbst ist ein umfangreiches Themengebiet, das nicht vollständig in diesem
Buch behandelt werden kann.
Prototypen und Emulatoren lassen sich beispielsweise mit Hilfe von FPGAs
konstruieren. Schaltschränke mit FPGA-Platinen lassen sich für Testfahrten im Kofferraum eines Autos unterbringen. Dabei ist dieser Ansatz nicht auf die Automobilindustrie beschränkt, auch in anderen Fällen werden Prototypen mit FPGAs gebaut.
Kommerziell verfügbare Emulatoren bestehen aus einer großen Anzahl von FPGAs.
Wenn solche Emulatoren verwendet werden, können Experimente mit Systemen
durchgeführt werden, die sich „fast” wie die endgültigen Systeme verhalten. Es ist
aber bereits bei nicht verteilten Systemen schwierig, Fehler durch Prototypen und
Emulation zu finden. Bei verteilten Systemen ist die Lage noch einmal komplizierter
(siehe z.B. [547]).
5.9 Formale Verifikation
Die formale Verifikation beschäftigt sich mit formalen mathematischen Beweisen,
welche die Korrektheit eines Systems zeigen11. Zur Durchführung einer formalen
Verifikation wird zuerst ein formales Modell benötigt. Wenn ein Modell erstellt
wurde, können damit bestimmte Eigenschaften bewiesen werden. Dieser Schritt ist
nur schwer zu automatisieren und erfordert einigen Aufwand. Wenn ein Modell
verfügbar ist, können wir versuchen, bestimmte Eigenschaften zu beweisen.
Die Techniken der formalen Verifikation können anhand der verwendeten Logik
klassifiziert werden:
• Aussagen-Logik: In diesem Fall bestehen die Modelle aus Booleschen Gleichungen. Zugehörige Werkzeuge heißen Tautologie-Checker oder Äquivalenz11 Dieser Text zu formaler Verifikation basiert auf einer Gastvorlesung von Tiziana Margaria-Steffen
an der TU Dortmund.
5 Bewertung und Validierung
Definition 5.43: Die Ausführung eines Modells eines Systems, in dem keine Komponente durch eine computerbasierte Simulation realisiert wird, heißt Rapid Prototyping. Dabei werden alle Bestandteile durch realistische Komponenten dargestellt.
Einige dieser Komponenten sollten nicht die endgültig verwendeten Komponenten
sein, da das System ansonsten dem realen System entspräche.
In vielen Fällen sollten Entwürfe in realistischen Umgebungen getestet werden, bevor
die endgültige Version produziert wird. Steuergeräte von Autos sind ein hervorragendes Beispiel hierfür. Diese Systeme sollten von Testfahrern in verschiedenen
Umgebungen verwendet werden, bevor sie in die Massenproduktion gehen. Daher
entwirft die Automobilindustrie Prototypen. Diese Prototypen sollten sich größtenteils wie die endgültigen Systeme verhalten, sie können dabei aber schwerer sein,
mehr Energie verbrauchen oder andere Eigenschaften besitzen, die einen Testfahrer
nicht stören. Der Begriff „Prototyp” kann für das gesamte System aus elektrischen
und mechanischen Komponenten verwendet werden. Die Unterscheidung zwischen
Rapid Prototyping und Emulation beginnt aber unscharf zu werden. Rapid Prototyping selbst ist ein umfangreiches Themengebiet, das nicht vollständig in diesem
Buch behandelt werden kann.
Prototypen und Emulatoren lassen sich beispielsweise mit Hilfe von FPGAs
konstruieren. Schaltschränke mit FPGA-Platinen lassen sich für Testfahrten im Kofferraum eines Autos unterbringen. Dabei ist dieser Ansatz nicht auf die Automobilindustrie beschränkt, auch in anderen Fällen werden Prototypen mit FPGAs gebaut.
Kommerziell verfügbare Emulatoren bestehen aus einer großen Anzahl von FPGAs.
Wenn solche Emulatoren verwendet werden, können Experimente mit Systemen
durchgeführt werden, die sich „fast” wie die endgültigen Systeme verhalten. Es ist
aber bereits bei nicht verteilten Systemen schwierig, Fehler durch Prototypen und
Emulation zu finden. Bei verteilten Systemen ist die Lage noch einmal komplizierter
(siehe z.B. [547]).
5.9 Formale Verifikation
Die formale Verifikation beschäftigt sich mit formalen mathematischen Beweisen,
welche die Korrektheit eines Systems zeigen11. Zur Durchführung einer formalen
Verifikation wird zuerst ein formales Modell benötigt. Wenn ein Modell erstellt
wurde, können damit bestimmte Eigenschaften bewiesen werden. Dieser Schritt ist
nur schwer zu automatisieren und erfordert einigen Aufwand. Wenn ein Modell
verfügbar ist, können wir versuchen, bestimmte Eigenschaften zu beweisen.
Die Techniken der formalen Verifikation können anhand der verwendeten Logik
klassifiziert werden:
• Aussagen-Logik: In diesem Fall bestehen die Modelle aus Booleschen Gleichungen. Zugehörige Werkzeuge heißen Tautologie-Checker oder Äquivalenz11 Dieser Text zu formaler Verifikation basiert auf einer Gastvorlesung von Tiziana Margaria-Steffen
an der TU Dortmund.