Formale Definition: Selmo-Automat

Wir definieren den Selmo-Automaten als ein 8-Tupel:

S=(Z,Σ,Γ,δ,λ,z0,B,M)

🔹 1. Z – Zustandsmenge

Die endliche Menge aller modellierten Zustände einer Selmo-Sequence (z. B. Init, Einlegen, Spannen, …)

---

🔹 2. Σ – Eingabealphabet

Die Menge aller relevanten Eingaben (Sensoren, Taster, Rückmeldesignale)

---

🔹 3. Γ – Ausgabealphabet

Die Menge aller möglichen Ausgangssignale (Ventile, Motoren, LEDs, etc.)

---

🔹 4. δ – Übergangsfunktion

δ:Z×Σ×M→Z

→ Der nächste Zustand wird bestimmt durch:

• den aktuellen Zustand

• die aktuellen Eingaben

• den Speicherzustand (Mem-Zonen)

Die Transition ist nur zulässig, wenn:

• alle S-Zonen erfüllt sind

• kein I (Interlock) verletzt ist

• CMZ (optional) keinen Fehler meldet

---

🔹 5. λ – Ausgabefunktion

λ:Z→Γ∗

→ Alle Ausgänge einer Zone werden bei Eintritt in einen Zustand gesetzt, wenn die Zone in der Bit-Control mit S versehen ist und einen Ausgang besitzt.

Dies entspricht der Moore-Logik: → Outputs hängen nur vom aktuellen Zustand ab, nicht vom Übergang.

---

🔹 6. z0 ∈ Z – Startzustand

Der initiale Zustand der Sequenz nach Freigabe

---

🔹 7. B : Z×X→{0,S,I, M} – Bit-Control-Matrix

Eine Kreuztabelle, die angibt:

• für jeden Zustand z∈Zz

• und jede Zone x ∈ X

→ welches Verhalten gilt:

• 0 = don't care

• S = erwartete Aktion (Steuerung oder Überwachung)

• I = Interlock (Sicherheitsüberwachung)

• M = Monitoring (Dokumentation der Abweichung ohne Reaktion)

---

🔹 8. M – Menge und Zustand aller Mem-Zonen

M={m1,m2,...,mk}, mi∈{0,1}

→ Jede Mem-Zone ist ein binärer Speicher, der durch S im Zustand gesetzt oder gelöscht wird. → Wird in der Übergangslogik (δ) verwendet, um Bedingungen zu speichern oder Entscheidungen zu ermöglichen.

---

🧩 Weitere logische Strukturen im Selmo-Automaten

🔸 Zonensystem X:

Zonen sind typisiert:

• Input-Zonen: liefern Zustände aus Sensoren

• Output-Zonen: aktivieren Aktoren

• In-Out-Zonen: Aktor + Sensor (mit Feedback)

• Mem-Zonen: reine logische Speicher

• Jede Zone ist einer oder mehreren Zuständen per Bit-Control zugeordnet

---

🔸 Interlock (I):

• Sobald eine Zone im Zustand mit i verknüpft ist, wird der aktuelle Signalzustand mit dem Sollwert verglichen.

• Bei Abweichung:

  • → Sequenzstopp

  • → Automatik-Release deaktiviert

  • → rote Fehlermeldung im HMI

---

🔸 Monitoring (M):

• Sobald eine Zone im Zustand mit M verknüpft ist, wird der aktuelle Signalzustand mit dem Sollwert verglichen.

• Bei Abweichung:

  • → Dokumentation

  • → Automatik-Release bleibt erhalten

  • → kein Fehlermeldung im HMI, aber dokumentiert in Historie

---

🔸 Sequence-Check (S):

• Steuert Aktoren (bei Output/In-Out)

• Erwartet Eingaben (bei Input/In-Out)

• → Zustand wird erst verlassen, wenn alle S-Zonen erfüllt sind

• → blaue HMI-Markierung zeigt aktive Erwartung

---

🔸 Speicherfunktion (Mem):

• Zustand setzt eine Mem-Zone → m=1

• Späterer Zustand setzt dieselbe Mem-Zone wieder zurück → m=0

• Der aktuelle Wert m kann Überwachung und Übergangsbedingung für δ sein

---

🔸 Erweiterbar um:

• CMZ (Constantly Monitoring Zones) → zustandsunabhängige Überwachung auf drei Ebenen (Sequence, HW-Zone, Plant)

• MXIC (Manual Cross Interlock) → Freigabebedingungen für Handtasten (z. B. HMI-Steuerung mit Sicherheitslogik)

• Parameter-Layer → modellierte Variablen wie Zeiten, Wiederholzahlen, Schwellenwerte

---

🏁 Fazit

Der Selmo-Automat ist ein vollständig formalisierter erweiterter Moore-Automat mit:

Eigenschaft	Ja / Nein
Deterministische Zustände	✅
Zustandsgesteuerte Ausgänge	✅
Signalüberwachung pro Zustand	✅
Logik für erlaubte Übergänge	✅
Automatische Fehlererkennung	✅
Interlock (Sicherheitsüberwachung)	✅
Speicherfunktionen (Mem-Zonen)	✅
Bedienerführung im HMI	✅
Erweiterte Diagnosefunktion	✅