 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Modellierung paralleler Programme |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Für die Modellierung paralleler Programme in Form von Kripke-Strukturen wird im Wesentlichen die gleiche Methode wie für die Modellierung sequentieller Programme verwendet, erweitert um einige für parallele Programme relevante Punkte.
Die Programme müssen auch hier in entsprechende logische Formeln übersetzt werden, wobei wiederum vorausgesetzt wird, dass die einzelnen Prozesse bereits nach der Methode zur Beschriftung sequentieller Programme beschriftet sind. Für das Gesamtprogramm wird zusätzlich folgende Erweiterung dieses Beschriftungsverfahrens eingeführt: Ausgehend von einem parallelen Programm P der Form P = cobegin P1 || P2 || ... || Pn coend sieht das entsprechende beschriftete Programm PL folgendermaßen aus: PL = cobegin l1: P1L l'1 || l2: P2L l'2 || ... || ln: PnL l'n coend Die Vorgehensweise bei der anschließenden Übersetzung der parallelen Programme in Logik erster Ordnung erfolgt wiederum induktiv über die Struktur der Programme. Zunächst beschreibt man die Startzustände des Programms P mit folgender Formel, wobei pre(V) eine Formel zur Beschreibung der entsprechenden initialen Variablenbelegungen ist: S0(V,PC) ≡ pre(V) ∧ pc = m ∧ Λni=1 (pci = ⊥) Für das Gesamtprogramm sieht die Übersetzungsprozedur dann folgendermaßen aus: C(l, cobegin l1: P1L l'1 || ... || ln: PnL l'n coend, l') ist die Disjunktion der folgenden drei Formeln: 1. Initialisierung des Programms: pc = l ∧ pc'1 = l1 ∧ ... ∧ pc'n = ln ∧ pc' = ⊥ 2. Terminierung des Programms: pc = ⊥ ∧ pc1 = l'1 ∧ ... ∧ pcn = l'n ∧ pc' = l' ∧ Λni=1 (pci = ⊥) 3. Ausführung des Programms entsprechend der Interleaving-Semantik: Λni=1 (C(li, Pi, l'i) ∧ same(V \ Vi) ∧ same(PC \ { pci })) Für Prozesse mit gemeinsamen Variablen (¬ same(V \ Vi)) ist die Einführung weiterer Arten von Anweisungen nötig (siehe Behandlung gemeinsamer Variablen). Rückkehr zu Modellierung von Programmen | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| Modellierung paralleler... | ||||
| ||||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
