An Overview of the Signal Clock Calculus - Informatik · C kombinatorisches Prädikat (kein...

Seminar über Programmiersprachen, Jennifer MöwertFachbereich Informatik

Fachbereich Informatik, Jennifer Möwert

An Overview of theSignal Clock Calculus



Inhaltsverzeichnis➢ Synchrone Programmiersprachen➢ Clock Calculus➢ Synchrone Paradigmen➢ SLTS➢ Clocks➢ SIGNAL➢ Definitionen➢ Endochrony➢ Bäume



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



SIGNAL

➢ Anfang der 80er Jahre

➢ Basiert auf synchronisiertem Datenfluss

➢ Systeme werden durch „Clocks“ beschrieben als relationale Spezifikationen

➢ Baut sequentielle Kontrollstrukturen auf



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



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



SCADE

➢ Nicht direkt Programmiersprache➢ Modellierungssprache➢ Von Herstellern von ESTEREL➢ Tool zur modellgetriebenen Softwareentwicklung

➢ Basiert auf LUSTRE ➢ Generiert C und Ada-Code



Clock Calculus

➢ Kompillierungsprozess in SIGNAL

➢ Analyse basiert auf theoretischen und implementationsverwandten Konzepten, nicht Standardobjekten („Clocks“), Techniken, Datenstrukturen („Clock Trees“) und spezialisierten Vokabeln



Ziel

➢ Konsistente Spezifikationen

➢ Automatisch Code generieren

➢ Effizienten Code generieren

➢ Synchronisationen sollen eingehalten werden



Synchrone Paradigmen

➢ Ausführung eines reaktiven Systems ist eine unendliche Sequenz von Reaktionen

➢ Eine Reaktion geschieht innerhalb eines logischen Moments



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



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



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



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)



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



SLTS

Screenshot von Seite 3 machen



Beispiel

Screenshot Seite 3 Beispiel



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



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



Clocks in SIGNAL

➢



Clocks in SIGNAL



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



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



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



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



Endochrony

➢ Bei LUSTRE ist initial eine Masterclock gegeben

➢ Also bei der Konstruktion bereits endochronous

➢ In SIGNAL endochronous nicht gewährleistet



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



Syntaktische Definition

➢ Charakterisiert durch Clock h und einer Funktion def(h) von condition Clocks

➢ H_1 op h_2 , wobei



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



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



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




➢ H_1 und h_2 teilen sich denselben Kontext, solange sie im gleichen Unterbaum a' sind

➢ Haben somit auch gleichen Vorfahr h




➢ 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




Bild von Seite 6 unten machen Für jede Clock k....

➢



Vielen Dank für Ihre Aufmerksamkeit!

An Overview of the Signal Clock Calculus - Informatik · C kombinatorisches Prädikat (kein...

Documents

Transcript of An Overview of the Signal Clock Calculus - Informatik · C kombinatorisches Prädikat (kein...