 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Modellierung von Programmen |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Bei Programmen handelt es sich im Prinzip zwar bereits um eine formale Modellierung von Systemen, im Kontext des Model Checking ist jedoch eine Modellierung in Form von Kripke Strukturen vorteilhaft, in die Programme demzufolge transformiert werden müssen.
Ein Programm besteht im einfachsten Fall aus Anweisungen, die sequentiell miteinander verknüpft sind. Um solche Programme in Form von Kripke-Strukturen zu modellieren, kann man eine Übersetzungsvorschrift C angeben, die ein textuell vorliegendes sequentielles Programm P in eine Formel R der Logik erster Ordnung umsetzt. Der Einfachheit halber kann man annehmen, dass jede Anweisung genau einen Anfangspunkt und genau einen Endpunkt hat und dass diese Punkte für jede Anweisung des Programms eindeutig beschriftet sind. Zunächst kann man also eine Beschriftungsvorschrift angeben, die zu einem unbeschrifteten Programm P ein beschriftetes Programm PL generiert (Details dazu unter Beschriftung sequentieller Programme). Ausgehend von einem solchermaßen beschrifteten Programm P kann man einen Programmzähler pc definieren, eine besondere Variable, deren Wertebereich die Programmbeschriftungen sowie ein undefinierter Wert ⊥ zur Symbolisierung der Programminaktivität sind. Mit einer logischen Formel, die aus der Konjunktion von Formeln über die Belegungen dieses Programmzählers und sowie aller Programmvariablen besteht, kann dann jederzeit der Zustand des Gesamtprogramms eindeutig beschrieben werden. Auf dieser Grundlage kann man dann die Übersetzungsvorschrift C induktiv über die Struktur von Anweisungsfolgen definieren. Sie hängt nur von drei Parametern ab: Der Beschriftung l des Anfangspunkts der Anweisungsfolge, der beschrifteten Anweisungsfolge P und der Beschriftung l' des Endpunkts der Anweisungsfolge (siehe Modellierung sequentieller Programme). Diese Übersetzungsvorschrift kann man mit einigen Erweiterungen auch für parallele Programme definieren. Parallele Programme bestehen aus einer Menge von sequentiellen Prozessen, die parallel zueinander ausgeführt werden können (vgl. Nebenläufige Systeme). Dabei geht man von einer Interleaving-Semantik des Programms aus, d.h. dass zu jedem Zeitpunkt maximal ein Prozess einen Arbeitsschritt ausführen kann. Jeder Prozess Pihat dabei seine eigene Menge Vi von Variablen, wobei die einzelnen Mengen jedoch nicht disjunkt sein müssen. Außerdem wird für jeden Prozess ein Programmzähler pi definiert (siehe Modellierung paralleler Programme). | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Modellierung von Programmen | ||||
| ||||
| ||||
| ||||
| ||||
 | Untergeordnet | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
| ||||
| ||||
| Ansprechpartner | | ||
| ||||
|
| | ||
| ||||
| Literaturhinweise | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
| ||||
| Glossar | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
