6.2 Formale Sicherheit durch deterministische Abläufe

Selmo basiert auf deterministischen Regeln. Das bedeutet: zu jeder Zeit existiert nur eine gültige Schaltstellung. Jeder Übergang ist eindeutig beschrieben und überprüfbar.

Das hat zwei entscheidende Konsequenzen:

1. Keine parallelen Logikzweige. Es gibt keine zwei Programme, die gleichzeitig dieselbe Variable verändern. Damit entfallen Race-Conditions und Mehrdeutigkeiten.

2. Sicherer Übergang zwischen Zuständen. Ein Zustand wird erst verlassen, wenn alle aktiven Zonen ihre Rückmeldung geliefert haben. Solange das nicht geschieht, bleibt das Schaltwerk stehen.

Dadurch sind alle Abläufe nicht nur logisch korrekt, sondern auch physikalisch überprüfbar.