Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
An Overview of theSignal Clock Calculus
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Inhaltsverzeichnis➢ Synchrone Programmiersprachen➢ Clock Calculus➢ Synchrone Paradigmen➢ SLTS➢ Clocks➢ SIGNAL➢ Definitionen➢ Endochrony➢ Bäume
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Synchrone Programmiersprachen
➢ Für eingebettete, Sicherheitskritische Systeme➢ Wichtiger Faktor: Die Zeit! ➢ Multi-Form-Time:➢ Durch Anzahl und Form der Eingabe bestimmt➢ Zero-delay model of circuits:➢ Programme bestehen aus linear ausgeführten Zuständen
➢ Determinismus → Verifikation einfacher➢ Kann alles, was wir mit endlichen Automaten ausdrücken können
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
SIGNAL
➢ Anfang der 80er Jahre
➢ Basiert auf synchronisiertem Datenfluss
➢ Systeme werden durch „Clocks“ beschrieben als relationale Spezifikationen
➢ Baut sequentielle Kontrollstrukturen auf
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
ESTEREL
➢ Anfang der 80er Jahre➢ Imperativ und synchron➢ Zusätzliche Statements in Bezug auf die Zeit benötigt
➢ Generiert Automaten → Zustände große Ausmaße annehmen
➢ Zeit wird durch sogenannte Events bestimmt➢ Beliebige Einheiten verwendbar
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
LUSTRE
➢ Auch Anfang 80er Jahre➢ Deklarativ und synchron➢ Ebenfalls für Sicherheitskritische Systeme verwendet
➢ Beispielsweise Notabschaltung der Kernkraftwerke und Steuerung des Airbus A320
➢ Die Zeit wird in diskreten Zeitpunkten gezählt➢ Automat wird erstellt → Verifikation erleichtert
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
SCADE
➢ Nicht direkt Programmiersprache➢ Modellierungssprache➢ Von Herstellern von ESTEREL➢ Tool zur modellgetriebenen Softwareentwicklung
➢ Basiert auf LUSTRE ➢ Generiert C und Ada-Code
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Clock Calculus
➢ Kompillierungsprozess in SIGNAL
➢ Analyse basiert auf theoretischen und implementationsverwandten Konzepten, nicht Standardobjekten („Clocks“), Techniken, Datenstrukturen („Clock Trees“) und spezialisierten Vokabeln
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Ziel
➢ Konsistente Spezifikationen
➢ Automatisch Code generieren
➢ Effizienten Code generieren
➢ Synchronisationen sollen eingehalten werden
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Synchrone Paradigmen
➢ Ausführung eines reaktiven Systems ist eine unendliche Sequenz von Reaktionen
➢ Eine Reaktion geschieht innerhalb eines logischen Moments
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Imperatives Paradigma
➢ Behandelt Empfang und Ausgabe von Events (Signale)
➢ Status „abwesend“ oder „präsent“ in einer Reaktion
➢ Wert in ESTEREL (imperativ) kann nur geändert werden, wenn dieser präsent ist
➢ Wert des Signals kann auch bei Abwesenheit gelesen werden
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Datenfluss Paradigma
➢ Stützt sich auf Berechnungen von Daten➢ Spezifikationen sind Systeme von Gleichungen
➢ Bestimmen Art der Berechnung einer Variablen
➢ Status „abwesend“ (*) und „präsent“ auch hier vorhanden
➢ Abwesende Variablen haben keinen signifikanten Wert
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
SLTS
➢Symbolic Labeled Transitions Systems
➢Abstrakte Maschine
➢Über Menge von Variablen S, einer Domain D und einer Menge von persistenten „memories“ M erstellt
➢Besteht aus Menge von Zuständen und Übergängen
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
SLTS➢ Valuation von V: S → D vereinigt {*} repräsentiert eine Reaktion eines Systems
➢ Zustand ist eine valuation von memories E: M → D
➢ I initialer Zustand (Initialisierungsprädikat)
➢ M Prädikat für memories
➢ C kombinatorisches Prädikat (kein Zustand)
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
SLTS
➢ M für Zustand des Systems zuständig, von außen nicht sichtbar
➢ C verbindet System mit der Umwelt, spezifiziert was innerhalb einer Reaktion passiert
➢ Paralleler Aufbau standard➢ Kernel von SIGNAL parallelenAufbauoperator I, Laufzeitoperator $, sowie Operatoren when, default und Funktionen
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
SLTS
Screenshot von Seite 3 machen
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Beispiel
Screenshot Seite 3 Beispiel
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Datenfluss Clocks
➢ Menge von Instanzen von Reaktionen➢ In imperativen Paradigmen auch „time scale“ genannt
➢ Aktiviert System, da parallele Berechnungen nicht notwendig sind
➢ Jeder Prozess eigene Aktivierungszeit → mehrere Clocks
➢ Werden zum Kommunizieren zwischen Komponenten gebraucht
➢ Bei LUSTRE geschieht Aktivierung durch Präsenz einer Eingabevariablen y
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Clocks in SIGNAL
➢ Häufige Verwendung
➢ Clock von y mit ŷ gekennzeichnet
➢ Jedes Objekt bezieht sich auf Berechnungen welche mit einer Clock verbunden ist
➢ Clocks beschreiben Mengen von valuations und Reaktionen
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Clocks in SIGNAL
➢
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Clocks in SIGNAL
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Spezifikationen in SIGNAL
➢ Relation in SIGNAL über Wert von präsenten Variablen und über den Zustand definiert
➢ Y:= x default z➢ Y ist präsent wenn x präsent ist oder z präsent➢ Clocks von Variablen sind nicht ausreichend➢ When Operator bringt booleschen Wert mit ein➢ Y:= x when c ➢ Y ist präsent wenn x präsent und c präsent und den Wert true hat
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Condition Clocks
➢ [c] element K➢ Kann mit booleschen Variablen umgehen➢ [c] Menge von Instanzen wo c mit dem Wert true präsent ist
➢ Semantische Berechnungsdomain {*, true, false}
➢ Durch condition Clocks in zwei Werte kodieren➢ Nun Clockvariablen (Relationen über Clocks) an propositionale Variablen (boolesche Gleichungen) angleichen
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Endochrony
➢ Komponente ist endochronous, wenn sie in einer asynchronen Umgebung ausgeführt werden kann, welche Eingabewerte unterstützt die keine Informationen über ihren Zustand haben
➢ Komponente hat somit keine Möglichkeit den Zustand einer Variablen deterministisch zu testen
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Endochrony
➢ Es kann nur ein Eingabeblock deterministisch getestet werden
➢ Deshalb muss endochronous Komponente eine Masterclock haben
➢ Diese ist einziger Eingabeblock von ausführbarem Code
➢ Andere Clocks passen sich rekursiv an
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Endochrony
➢ Bei LUSTRE ist initial eine Masterclock gegeben
➢ Also bei der Konstruktion bereits endochronous
➢ In SIGNAL endochronous nicht gewährleistet
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Bäume
➢ Verwendete Datenstruktur➢ Knoten stellen Clockvariable dar➢ Für zwei Knoten n_1 und n_2 , „n_1 ist Nachkomme von n_2“ bedeutet „ Clock n_1 ist in Clock n_2 enthalten“
➢ Ziel: Größe der Definitionen minimieren➢ Es gibt die syntaktische und semantische Definition
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Syntaktische Definition
➢ Charakterisiert durch Clock h und einer Funktion def(h) von condition Clocks
➢ H_1 op h_2 , wobei
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Clocks in Bäumen
➢ Standard Bäume (Partition Trees)
➢ Bei LUSTRE Synchronisationen ist Wurzel die Masterclock
➢ Tiefensuche gibt Anzahl von Berechnungen von Definitionen an
➢ Kontrollstrukturen leiten sich von Baumstruktur ab
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Konstruktion von Bäumen
➢ Erst alle Teilbäume erstellt und zu einem Baum zusammen gefügt
➢ Jede Clockvariable stellt Wurzel des Teilbaums dar
➢ Algorithmus iteriert folgenden Prozess:➢ Wähle Clockvariable h_3 vom Typ h_1 op h_2, wobei h_1 und h_2 zu Baum a' gehören
➢ Berechnungen von def(h_3) und Einfügungen eines Unterbaums a, dessen Wurzel h_3 in a' ist
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Eigenschaften eines Unterbaums
➢ Unterbaum a enthält Menge von condition Clocks, von denen andere Clocks definiert werden können (Kontext)
➢ Einhaltung zweier Prinzipien:➢ Jede Clock h in a ist var(h) mit zugehörigem Kontext
➢ Tiefensuche findet alle Variablen von var(h) vor h
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Eigenschaften eines Unterbaums
➢ H_1 und h_2 teilen sich denselben Kontext, solange sie im gleichen Unterbaum a' sind
➢ Haben somit auch gleichen Vorfahr h
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Eigenschaften eines Unterbaums
➢ Wenn Baum endochronous ist, ist Masterclock die Wurzel
➢ Es werden Definitionen zu h_1 op h_2 berechnet
➢ Sollte ein solcher Ausdruck nicht in den Regeln gefunden werden → rewriting Regeln
➢ Rewriting System ist ad-hoc und unvollständig➢ Nach dem Anwenden der Regeln kein geeigneter Ausdruck → Analyse hält an
➢ Ist nicht endochronous
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Eigenschaften eines Unterbaums
Bild von Seite 6 unten machen Für jede Clock k....
➢
Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik
Fachbereich Informatik, Jennifer Möwert
Vielen Dank für Ihre Aufmerksamkeit!