Anforderungen an den Sicherheitskern (REQ-IXL)

Umgesetzt in crates/railit-kernel. Nachweise in crates/railit-kernel/tests/kernel.rs, crates/railit-kernel/tests/phase2.rs, crates/railit-kernel/tests/borders.rs (Streckenblock mit zwei bzw. drei echten Kernen, Property-Tests mit Laufzeiten und Neustarts), im Property-Test crates/railit-kernel/tests/invariants.rs und in den Szenarien unter tests/scenarios/.

ID	Anforderung	Gefährdung	Nachweis
REQ-IXL-001	Der Kern ist eine deterministische Funktion von Zustand, Zeit und Eingaben: keine I/O, keine Uhr, keine Allokation, keine Panikpfade, kein unsafe.	H-007	kernel_is_deterministic; Lints (deny) in lib.rs; no_std-Build ohne Allokator in der CI
REQ-IXL-002	Feindliche Fahrstraßen sind nie gleichzeitig eingestellt.	H-001	conflicting_routes_are_rejected, Invariante no_conflicting_routes, Property-Test, Szenario 03
REQ-IXL-003	Eine Fahrstraße wird nur zugelassen, wenn keine feindliche Fahrstraße eingestellt ist, alle Abschnitte des Fahrwegs frei gemeldet und unverschlossen sind, die Abschnitte des Durchrutschwegs keinem anderen Durchrutschweg gehören, keine Weiche einen Verschluss in anderer Lage trägt, umzustellende Weichen von Durchrutschweg und Flankenschutz in freien Abschnitten liegen und das Startsignal nicht als Schutzsignal gehalten wird.	H-001, H-005	occupied_or_disturbed_sections_block_routes, continuation_may_use_the_overlap, flank_signals_are_held_at_stop, Szenarien 07 und 08
REQ-IXL-004	Eine Weiche wird nur gestellt, wenn sie nicht im Fahrweg verschlossen ist (außer durch die anfordernde Fahrstraße während der Einstellung), kein Verschluss eine andere Lage verlangt und ihr Abschnitt frei ist (außer bei der bestätigten Hilfshandlung „Weiche umstellen“).	H-003	single_point_operation, aux_force_point, Prüfung in command_point, Property-Test
REQ-IXL-005	Ein Signal zeigt nur Fahrt, solange alle Weichen von Fahrweg, Durchrutschweg und Flankenschutz überwacht in Lage, alle Abschnitte von Fahrweg und Durchrutschweg frei, die Schutzsignale in Halt, die Bahnübergänge geschlossen gemeldet und das Signal intakt ist. Fällt eine Bedingung weg, fällt es sofort auf Halt und zeigt erst nach erneuter Bedienung wieder Fahrt.	H-001, H-002, H-010	signal_drops_when_point_loses_supervision, signal_drops_when_section_ahead_is_occupied, occupied_overlap_blocks_proceed, Invariante proceed_only_when_safe, Szenario 04
REQ-IXL-006	Wird eine Fahrstraße nach der Fahrtstellung zurückgenommen, bleibt sie für den Zeitverschluss festgelegt. Fährt währenddessen ein Zug ein, wird alarmiert und die Fahrstraße bleibt verschlossen.	H-001, H-009	cancelling_respects_time_lock, train_entering_cancelled_route_keeps_locks, Szenario 05
REQ-IXL-007	Fahrstraßen werden zugbewirkt in Fahrtrichtung aufgelöst: ein Abschnitt (mit seinen Weichen, den ihn schützenden Flankenschutzmaßnahmen und den Bahnübergängen darin) erst, wenn der Zug ihn befahren und geräumt hat und im folgenden Abschnitt ist. Erreicht der Zug den Zielabschnitt, wird der Fahrweg aufgelöst; der Durchrutschweg bleibt bis zur Auflösezeit festgelegt und wird nur aufgelöst, wenn keiner seiner Abschnitte unverschlossen besetzt ist.	H-001, H-003	route_lifecycle_with_partial_release, overlap_release_waits_for_time_and_vacancy, flank_protection_is_released_with_its_section, Szenarien 01 und 02
REQ-IXL-008	Nach jedem Zyklus werden die Invarianten geprüft; dabei werden alle Verschlüsse und Haltezähler unabhängig aus den Fahrstraßen neu berechnet. Eine Verletzung führt in den sicheren Zustand: alle Signale Halt, Ersatzsignale aus, keine Stellbefehle, alle Anforderungen abgelehnt. Beim Start erhalten alle Signale Halt und alle Bahnübergänge einen Stellbefehl.	H-007	invariant_violation_enters_safe_state, first_cycle_commands_stop_everywhere, Property-Test
REQ-IXL-009	Fehlende oder veraltete Meldungen gelten als gestört; gestört wird wie besetzt behandelt.	H-005	nothing_is_clear_without_reports, stale_reports_drop_the_signal
REQ-IXL-010	Erreichen die Weichen einer Fahrstraße ihre Lage nicht innerhalb der Umstellzeit, wird die Einstellung abgebrochen und alarmiert.	H-002	setting_times_out_when_points_do_not_move, Szenario 06
REQ-IXL-011	Wird ein frei gemeldeter Abschnitt besetzt, ohne dass eine erlaubte Fahrt hineinführt (Fahrstraße mit Fahrt, befahren, haltgefallen, in Rücknahme, angekommen oder mit Ersatzsignal) und ohne dass er ein unverschlossener Einfahrabschnitt an der Netzgrenze ist, wird alarmiert. Fährt ein Zug in eine nur festgelegte Fahrstraße ein, wird eine Haltüberfahrung gemeldet; die Fahrstraße bleibt verschlossen.	H-009	unauthorized_occupancy_is_alarmed, signal_passed_at_danger, Szenario 11
REQ-IXL-012	Der Durchrutschweg wird mit der Fahrstraße verschlossen: seine Abschnitte exklusiv (eine anschließende Fahrstraße darf sie als Fahrweg nutzen), seine Weichen lagebezogen.	H-001, H-009	overlap_is_locked_and_points_are_set, continuation_may_use_the_overlap, Szenario 08
REQ-IXL-013	Flankenschutz wird mit der Fahrstraße hergestellt: Schutzweichen werden lagebezogen verschlossen (auch von mehreren Fahrstraßen zugleich), Schutzsignale in Halt gehalten.	H-001	flank_signals_are_held_at_stop, Szenario 08
REQ-IXL-014	Hilfshandlungen (Fahrstraßenhilfsauflösung, Achszählgrundstellung, Ersatzsignal, Weiche im gestörten Abschnitt umstellen) werden nur ausgeführt, wenn ein zweiter, anderer Bediener sie innerhalb der Bestätigungsfrist bestätigt und ihre Voraussetzungen bei der Bestätigung noch gelten. Jede Ausführung erhöht das Zählwerk; nicht bestätigte Anforderungen verfallen.	H-006	aux_needs_a_second_operator_in_time, aux_release_of_occupied_route, aux_reset_tvd, aux_force_point, Szenarien 10 und 12
REQ-IXL-015	Das Ersatzsignal (Zs1) leuchtet nur für eine festgelegte oder haltgefallene Fahrstraße, deren Weichen in Lage, Schutzsignale in Halt und Bahnübergänge geschlossen sind. Es erlischt bei Einfahrt des Zuges, nach seiner Höchstdauer oder sobald eine Bedingung entfällt. Eine Rücknahme bei leuchtendem Zs1 unterliegt dem Zeitverschluss.	H-001, H-009	substitute_signal_lets_train_pass, substitute_signal_times_out_and_drops, cancel_with_substitute_uses_time_lock, Invariante substitute_only_when_justified, Szenario 10
REQ-IXL-016	Ein Bahnübergang wird geschlossen, sobald eine Fahrstraße über ihn eingestellt wird, und bleibt geschlossen, solange eine Fahrstraße ihn braucht und solange sein Abschnitt nicht frei ist.	H-010	level_crossing_must_be_closed_before_proceed, level_crossing_opens_after_train_has_left, Invariante shared_locks_match_routes, Szenario 09
REQ-IXL-017	An jeder Bereichsgrenze hält höchstens eine Seite die Erlaubnis. Übergabe nur als Angebot mit fortlaufender Nummer, das nur mit größerer Nummer und nicht vor Ablauf der Einschwingzeit nach einem (Neu-)Start angenommen wird; das Angebot endet mit der Quittung. Ohne Angebot übernimmt nur der beim Anlauf bestimmte Kern oder die bestätigte Hilfshandlung „Erlaubnis zurückholen“ die Erlaubnis, und erst nachdem der Nachbar die Einschwingzeit lang gemeldet hat, sie nicht zu halten. Hält ein Kern die Erlaubnis und meldet der Nachbar dasselbe, wird alarmiert.	H-012	Property-Test never_both_sides_hold_permission (zwei Kerne, Laufzeiten bis 1 s, Neustarts), designated_side_takes_permission_after_settle_time, only_newer_offers_are_taken, take_back_permission_by_aux_operation, permission_conflict_is_alarmed
REQ-IXL-018	Die Erlaubnis wird nur auf Anforderung des Nachbarn abgegeben, wenn keine Fahrstraße über die Grenze eingestellt ist, der eigene Annäherungsabschnitt frei und nur von Fahrstraßen ab dem Einfahrsignal belegt ist, seine Weichen nicht anders verschlossen sind, der Nachbar seinen Annäherungsabschnitt frei meldet und der Kern die Erlaubnis nicht selbst angefordert hat. Mit der Abgabe wird der Annäherungsabschnitt im selben Zyklus verschlossen.	H-012	permission_is_given_only_when_safe
REQ-IXL-019	Ohne Erlaubnis ist der Annäherungsabschnitt verschlossen: Seine Abschnitte stehen nur Fahrstraßen ab dem Einfahrsignal offen, seine Weichen sind in Lage verschlossen. Züge des Nachbarn dürfen ihn ohne Alarm besetzen.	H-001, H-012	incoming_trains_are_authorized_only_without_permission, Invariante borders_are_consistent
REQ-IXL-020	Eine Fahrstraße über die Grenze wird nur mit Erlaubnis zugelassen. Ihr Signal zeigt nur Fahrt, solange die Erlaubnis gehalten wird und eine aktuelle Meldung des Nachbarn dessen Annäherungsabschnitt frei, gesichert und ausschließlich verschlossen meldet; fällt die Verbindung aus, fällt das Signal auf Halt und es wird alarmiert.	H-001, H-012	exit_needs_permission_and_clear_neighbour, lost_neighbour_drops_exit_signal, Invariante proceed_only_when_safe
REQ-IXL-021	Überdecken sich die Annäherungsabschnitte mehrerer Grenzen eines Bereichs (eingleisige Strecke zwischen zwei Bahnhöfen), gibt der Bereich eine Erlaubnis nur ab, solange keine andere Grenze den Abschnitt verschließt, und meldet einen doppelt verschlossenen Abschnitt keinem Nachbarn als ausschließlich verschlossen. Damit schicken nie zwei Nachbarn zugleich Züge in denselben Abschnitt.	H-012	Property-Test never_two_stations_feed_the_single_track (drei Kerne; findet ohne die Regel eine Gegenfahrt), single_track_direction_changes_in_order, Szenario 13
REQ-IXL-022	Die Bestätigung einer Hilfshandlung wiederholt die Hilfshandlung (Art, Element, Lage). Weicht sie von der offenen ab, wird nichts ausgeführt, die offene Hilfshandlung verfällt und muss neu angefordert werden. Damit kann eine falsche Anzeige beim bestätigenden Bediener nie zur Ausführung einer anderen Hilfshandlung führen.	H-006, H-016	confirmation_must_restate_the_operation, Property-Test der Invarianten mit zufällig wiederholter Hilfshandlung, Szenario 12
REQ-IXL-023	Die Invariantenprüfung (REQ-IXL-008) ist linear in der Größe des Plans und der eingestellten Fahrstraßen: Jede Aussage wird in zwei Richtungen geprüft (jede eingestellte Fahrstraße hat ihre Verschlüsse; es gibt keine weiteren, exklusive gezählt, geteilte durch Abziehen von den Zählern). Sie meldet genau dann eine Verletzung, wenn die direkte, quadratische Fassung es tut, und hinterlässt den Zustand bitgleich.	H-007	linear_check_agrees_with_reference, kernel_never_becomes_unsafe
REQ-IXL-024	Leistung (Konzept, Abschnitt 15): Bei 5000 Elementen, die in jedem Zyklus alle melden, und laufenden Fahrstraßenanforderungen bleibt der Kernzyklus im 99. Perzentil unter 1 ms und die Zulassungsprüfung einer Fahrstraße unter 10 µs. Die CI misst das mit railit bench --check und schlägt bei Überschreitung fehl.	H-015	bench_measures_a_small_corridor, railit bench --check (CI-Job „Leistung“)
REQ-IXL-025	Übernahme des Betriebs (REQ-SVC-012): Der Kern übernimmt einen mitgelesenen Zustand nur restriktiv angeglichen – jede Fahrstraße mit Fahrt fällt auf Halt (nur Rücknahme möglich), alle Signale auf Halt, alle Ersatzsignale aus, offene Hilfshandlungen verfallen, die Einschwingzeit beginnt neu; Verschlüsse und alle übrigen Phasen bleiben unverändert. Danach gelten die Invarianten, sonst geht der Kern in den sicheren Zustand; das vollständige Stellbild geht an das Feld.	H-001, H-003, H-015, H-017	proceed_falls_to_halt_and_locks_remain, locked_route_and_train_in_route_continue, pending_aux_expires_and_substitute_goes_out, safe_state_is_kept, kernel_never_becomes_unsafe
REQ-IXL-026	Eine gekoppelte Weiche wird nur mit ihrer Partnerweiche gestellt (REQ-TOP-017): Das Einzelstellen ist nur zulässig, wenn auch die Partnerweiche unverschlossen und ihr Abschnitt frei ist, und befiehlt beide Weichen in gekoppelter Lage. Die Hilfshandlung „Weiche umstellen“ verlangt zusätzlich eine unverschlossene Partnerweiche, deren Abschnitt gestört oder frei ist, und stellt beide. Fahrstraßen stellen und verschließen die Partnerweiche über ihren Flankenschutz (REQ-PLN-021). Am Feld hängen gekoppelte Weichen an einem Antrieb: Über EULYNX ist eine Kopplung ein Feldelement (benannt nach der ersten Weiche); Stellbefehle an die zweite gehen in gekoppelter Lage an dieses Element, seine Lagemeldung gilt für beide, und der Simulator lässt beide gemeinsam umlaufen.	H-002, H-003	single_move_takes_the_partner_along, route_locks_all_four_points, forced_move_takes_the_partner_along, coupled_points_share_one_drive, Szenarien 25 und 27