## Blatt 3

### Aufgabe 5

---

#### Global

##### 1. Während der Zug den Bahnübergang passiert, muss die Schranke geschlossen sein:
\begin{align*}
Sys \models \textbf{G }(& (Zug.d >= Welt.GP \land Zug.d < Welt.SP \land \textbf{F } Zug.d >= Welt.SP)\\
& \Rightarrow (Schranke.neigungswinkel = 0 \textbf{ U } Zug.d >= Welt.SP)
\end{align*}

##### 2. Der Zug hat entweder den Sensorpunkt passiert oder vor dem Gefahrenpunkt angehalten:
\begin{align*}
Sys \models \textbf{F G }(Zug.d > Welt.SP \land Zug.v > 0) \lor \textbf{F G }(Zug.d < GP \land Zug.v = 0)
\end{align*}

##### 3. Wenn ein Schließbefehl gesendet wird, ist die Schranke irgendwann geschlossen:
\begin{align*}
Sys \models \textbf{G }(&Funkkanal.ZugZuUebergang = schliessbefehl \\
&\Rightarrow \textbf{F }(Schranke.neigungswinkel = 0))
\end{align*}

##### 4. Die Schranke schließt sich nur, wenn ein Schließbefehl gesendet wurde:
\begin{align*}
Sys \models (Schranke.neigungswinkel = 90)\textbf{ U }(Funkkanal.ZugZuUebergang = schliessbefehl)
\end{align*}

##### 5. Freigabe wird nur gesendet, wenn davor eine Anfrage gesendet wurde:
\begin{align*}
Sys \models (Funkkanal.UebergangZuZug = leer)\textbf{ U }(Funkkanal.ZugZuUebergang = statusanfrage)
\end{align*}

##### 6. Freigabe wird nur gesendet, wenn der Bahnübergang gesichert ist:
\begin{align*}
Sys \models \textbf{G }(Funkmodul.UebergangZuZug = freigabe \Rightarrow Schranke.neigungswinkel = 0)
\end{align*}

##### 7. Zug bremst nicht bevor er BEP ohne Freigabe passiert:
\begin{align*}
Sys \models (Bremse.verzoegerung = 0) \textbf{ U } (&Zug.d >= Welt.GP - Welt.z - \frac{Zug.v^2}{2\cdot Welt.a} \\
& \land Funkkanal.UebergangZuZug \neq freigabe))
\end{align*}

##### 8. Zug bremst, wenn er keine Freigabe erhalten hat und hinter dem BEP ist:
\begin{align*}
Sys \models &\left( Funkkanal.UebergangZuZug \neq freigabe \textbf{ U } Zug.d >= Welt.GP - Welt.z - \frac{Zug.v^2}{2\cdot Welt.a} \right) \\
&\Rightarrow \textbf{G } ( Zug.d >= Welt.GP - Welt.z - \frac{Zug.v^2}{2\cdot Welt.a} \Rightarrow Bremse.verzoegerung > 0 )
\end{align*}

##### 9. Zug passiert den Gefahrenpunkt nur, wenn er eine Freigabe erhalten hat:
\begin{align*}
Sys \models (Zug.d < GP)\textbf{ U }(Funkkanal.UebergangZuZug = freigabe)
\end{align*}

---

#### Bahnübergang

##### 1. Die Schranke ist am Ende geöffnet:
\begin{align*}
Sys \models \textbf{F G }(Schranke.neigungswinkel = 90)
\end{align*}

##### 2. Die Schranke ist nach Ablauf des Timers oder nachdem der Zug passiert ist nicht mehr geschlossen:
\begin{align*}
Sys \models \textbf{G }(&Timer = Abgelaufen \lor ZugSensor = True\\
& \Rightarrow \textbf{XXX }(Schranke.neigungswinkel \neq 0))
\end{align*}

##### 3. Wenn der Schrankenmotor sichert, verringert sich der Neigungswinkel der Schranke:
\begin{align*}
Sys \models \textbf{G }(&Uebergangssteuerung.motor = sichern \\
& \land Schranke.neigungswinkel > 0 \\
& \Rightarrow \exists x ( Schranke.neigungswinkel = x \land \textbf{X } (Schranke.neigungswinkel < x)))
\end{align*}

\begin{align*}
Sys \models \textbf{G }(&Uebergangssteuerung.motor = sichern \\
& \land Schranke.neigungswinkel > 0 \\
& \Rightarrow ( Schranke.neigungswinkel < next(Schranke.neigungswinkel)))
\end{align*}

##### 4. Wenn der Schrankenmotor entsichert, vergrößert sich der Neigungswinkel der Schranke:
\begin{align*}
Sys \models \textbf{G }(& Uebergangssteuerungsteuerung.motor = entsichern \\
& \land Schranke.neigungswinkel < 90 \\
& \Rightarrow \exists x ( Schranke.neigungswinkel = x \land \textbf{X } (Schranke.neigungswinkel > x)))
\end{align*}

---

#### Zug

##### 1. Sobald der Zug einmal angehalten hat, darf er nicht mehr weiterfahren:
$$
Sys \models \textbf{G }(Zug.v = 0 \Rightarrow (\textbf{G } Zug.v = 0))
$$

##### 2. Sobald angefangen wird zu bremsen, ist die Geschwindigkeit des Zuges irgendwann 0:
$$
Sys \models \textbf{G }(Bremse = Aktiv \Rightarrow \textbf{F } Zug.v = 0 )
$$

##### 3. Wenn die Bremse aktiv ist, verringert sich die Geschwindigkeit bis der Zug hält:
$$
Sys \models \textbf{G }(Bremse = Aktiv \land Zug.v > 0 \Rightarrow \exists x ( Zug.v = x \land \textbf{X } (Zug.v < x)))
$$

##### 4. Die Zugsteuerung erreicht irgendwann einen Endzustand:
$$
Sys \models \textbf{F }(Zugsteuerung = FahrenNachBEP \lor Zugsteuerung = ZugHaeltVorGP)
$$

##### 5. Zug bremst, obwohl Bahnübergang geschlossen:
$$
Sys \models \textbf{G }(Schranke.neigungswinkel = 0 \Rightarrow Zug.v > 0)
$$

---

#### Sensoren

##### 1. Der SchrankeOffenSensor gibt den Zustand der Schranke wieder (mit einem Schritt Verzögerung):
$$
Sys \models \textbf{G }(Schranke.neigungswinkel = 90 \Leftrightarrow \textbf{X }(SchrankeOffenSensor = True))
$$

##### 2. Der SchrankeGeschlossenSensor gibt den Zustand der Schranke wieder (mit einem Schritt Verzögerung):
$$
Sys \models \textbf{G }( Schranke.neigungswinkel = 0 \Leftrightarrow \textbf{X }(SchrankeGeschlossenSensor = True))
$$

##### 3. Der ZugSensor meldet das Passieren des Zuges erst, wenn dieser den ZugSensor passiert hat (mit einem Schritt Verzögerung):
$$
Sys \models \textbf{G }(Zug.d >= Welt.SP \Leftrightarrow \textbf{X }(ZugSensor = True))
$$

##### 4. Das Hodometer misst den korrekten Abstand zum Bahnübergang (mit einem Schritt Verzögerung):
$$
Sys \models \textbf{G }(\exists d'. Zug.d = d' \land \textbf{X } Hodometer.dGemessen = d')
$$

##### 5. Das Hodometer misst die korrekte Geschwindigkeit (mit einem Schritt Verzögerung):
$$
Sys \models \textbf{G }(\exists v' . Zug.v = v' \land \textbf{X }(Hodometer.vGemessen = v'))
$$

# Blatt 5

Zug auf ungesichertem Bahnübergang:

\begin{align*}
Sys \models \textbf{G } (&(Zug.d >= Welt.GP \land Zug.d < Zug.SP) \\
& \implies ((\textbf{G } Schranke.neigungswinkel = 0) \\
& \lor (Schranke.neigungswinkel = 0 \textbf{ U } Zug.d >= Welt.SP) ))
\end{align*}

### DCCA:

#### Überprüfung

##### Einelementige

* BremseFehler: :heavy_check_mark:
* SchrankeGeschlossenSensorFehler, false negative: :heavy_check_mark:
* SchrankeGeschlossenSensorFehler, false positive: :x:
* ZugsensorFehler, false positive: :x:
* ZugsensorFehler, false negative: :heavy_check_mark:
* SchrankenmotorFehler, Failure: :heavy_check_mark:
* SchrankenmotorFehler, SlowDown: :heavy_check_mark:
* Hodometer, Deviation: :x:
* Hodometer, Failure: :x:
* ZugfunkmodulFehler: :heavy_check_mark:
* ÜbergangsfunkmodulFehler: :heavy_check_mark:

##### ZweiElementige

* BremseFehler
* SchrankeGeschlossenSensorFehler, false negative: :heavy_check_mark:
* ZugsensorFehler, false negative: :heavy_check_mark:
* SchrankenmotorFehler, Failure: :x:
* SchrankenmotorFehler, SlowDown: :heavy_check_mark:
* ZugfunkmodulFehler: :x:
* ÜbergangsfunkmodulFehler: :x:

* SchrankeGeschlossenSensorFehler, false negative
* ZugsensorFehler, false negative: :heavy_check_mark:
* SchrankenmotorFehler, Failure: :heavy_check_mark:
* SchrankenmotorFehler, SlowDown: :heavy_check_mark:
* ZugfunkmodulFehler: :heavy_check_mark:
* ÜbergangsfunkmodulFehler: :heavy_check_mark:

* ZugsensorFehler, false negative
* SchrankenmotorFehler, Failure: :heavy_check_mark:
* SchrankenmotorFehler, SlowDown: :heavy_check_mark:
* ZugfunkmodulFehler: :heavy_check_mark:
* ÜbergangsfunkmodulFehler: :heavy_check_mark:

* SchrankenmotorFehler, Failure
* ZugfunkmodulFehler: :heavy_check_mark:
* ÜbergangsfunkmodulFehler: :heavy_check_mark:

* SchrankenmotorFehler, SlowDown
* ZugfunkmodulFehler: :heavy_check_mark:
* ÜbergangsfunkmodulFehler: :heavy_check_mark:

* ZugfunkmodulFehler
* ÜbergangsfunkmodulFehler: :heavy_check_mark:

##### Mit Monotonieeigenschaft von sicheren Mengen

* SchrankenGeschlossenSensorFehler, false negative; ZugsensorFehler, false positive, SchrankenMotorFehler, Failure; SchrankenMotorFehler, SlowDown: :heavy_check_mark:

* BremseFehler; SchrankeGeschlossenSensorFehler, false negative; ZugsensorFehler, false negative; SchrankenmotorFehler, SlowDown; :heavy_check_mark:

### Minimal Critial Sets

**{SchrankeGeschlossenSensor (false positive)}**: Freigabe wird gesendet obwohl die Schranke nicht geschlossen ist.

**{ZugsensorFehler (false positive)}**: Der Sensor detektiert fälschlicherweise eine Zug, wodurch die Schranke geöffnet wird während der Zug den Übergang passiert.

**{Hodometer (Deviation)}**: Die Punkte werden falsch berechnet und der Zug sendet die Anfragen an den Bahnübergang zu einem falschen Zeitpunkt.

**{Hodometer (Failure)}**: Die Position des Zuges wird nicht geupdated, sodass keine Schliessbefehl an den Bahnübergang gesendet wird und der Zug nicht das Passieren des Bremseinsatzpunktes erkennt.

**{Bremse (Failure), Schrankenmotor (Failure)}**: Die Schranke wird nicht geschlossen und der Zug kann nicht bremsen.

**{Bremse (Failure), Zugfunkmodul (Failure)}**: Der Zug sendet keinen Schließbefehl und der Zug kann auch nicht bremsen.

**{Bremse (Failure), Übergangsfunkmodul (Failure)}**: Der Bahnübergang erhält keinen Schließbefehl und der Zug kann auch nicht bremsen.

### Erklärung von Unterschieden zu Aufgabe 2
* Wir haben nicht genau aufgezeigt, wieso die Schranke nicht geschlossen ist.
* Wir haben beim Hodometer nicht zwischen Ausfall und Messfehlern unterschieden.
* Wir haben nicht betrachtet, wieso keine Freigabe gesendet / empfangen wird.