Anforderungen an Projektierung und Plan-Image (REQ-PLN)

Umgesetzt in crates/railit-plan und crates/railit-planning. Das Plan-Image hat das Format v5 (Durchrutschwege, Flankenschutz, Bahnübergänge, Signalarten und -systeme, Grenzen, Längen, gekoppelte Weichen). Nachweise in crates/railit-plan/tests/image.rs, crates/railit-planning/tests/planning.rs und crates/railit-planning/tests/slip.rs.

Plan-Image

ID	Anforderung	Gefährdung	Nachweis
REQ-PLN-001	Der Kern arbeitet nur mit einem Plan, der vollständig geprüft wurde (PlanView::parse). Ein teilweise gültiger Plan wird nie verwendet.	H-004	Typsystem: PlanView entsteht nur über parse; railit_runtime::load_plan
REQ-PLN-002	Inkonsistente Pläne werden abgewiesen: ungültige Verweise, leere Fahrstraßen, doppelte Weichen oder Abschnitte, Weichen außerhalb der Abschnitte ihrer Fahrstraße, unsymmetrische oder reflexive Feindlichkeiten, ungültige Namen.	H-004	inconsistent_plans_are_rejected
REQ-PLN-003	Jede Veränderung des Images wird erkannt (SHA-256 über den gesamten Inhalt).	H-004, H-008	every_single_bit_flip_is_detected (jedes Byte, mehrere Bits)
REQ-PLN-004	Ein Plan kann mit Ed25519 signiert werden. railitd startet nur mit einem Plan, dessen Signatur zum hinterlegten Schlüssel passt; unsignierte Pläne nur mit ausdrücklicher Freigabe (--allow-unsigned).	H-008	signatures_are_checked, unsigned_or_foreign_plans_are_refused (railitd), keygen_compile_verify_info (CLI)

Projektierung

ID	Anforderung	Gefährdung	Nachweis
REQ-PLN-010	Hauptsignale (auch Mehrabschnittssignale, ETCS-Halt-Tafeln) stehen am Gleisende in Wirkrichtung oder höchstens 30 m davor (PlanningConfig::signal_gap), ohne Bahnübergang oder Kreuzungsstelle dazwischen, und dahinter beginnt ein anderer Gleisfreimeldeabschnitt. Die Längen im Plan zählen ab dem Signal: Fahrweg mit dem Rest des Startgleises und ohne das Stück hinter dem Zielsignal, Durchrutschweg und Annäherungsabschnitt ab dem Signal.	H-001, H-005	signals_must_stand_at_tvd_boundaries, signals_may_stand_shortly_before_the_tvd_boundary
REQ-PLN-011	Fahrstraßen werden vollständig erzeugt: jeder Weg von einem Startsignal bis zum nächsten Hauptsignal gleicher Richtung oder einem Netzende, mit allen Weichenlagen und den Abschnitten in Fahrreihenfolge.	H-001, H-002	example_routes_are_generated, Property-Test ladder_stations_plan_and_verify
REQ-PLN-012	Zwei Fahrstraßen sind feindlich, wenn sie (1) dasselbe Startsignal haben, (2) einen Abschnitt oder (3) eine Weiche des Fahrwegs teilen, (4) der Durchrutschweg der einen im Fahrweg der anderen liegt – außer die andere beginnt am Zielsignal der einen (anschließende Fahrstraße), (5) ihre Durchrutschwege einen Abschnitt teilen, (6) sie für eine Weiche (Fahrweg, Durchrutschweg oder Flankenschutz) verschiedene Lagen verlangen oder (7) die eine an einem Schutzsignal der anderen beginnt.	H-001	example_routes_are_generated, example_phase2_data, ladder_stations_plan_and_verify
REQ-PLN-013	Ein zweites, unabhängig aufgebautes Verfahren prüft jeden Plan gegen das Netz (Fahrstraßen, Feindlichkeiten, Elemente). Nur übereinstimmende Pläne werden geschrieben; das geschriebene Image wird zurückgelesen und verglichen.	H-004	verification_detects_tampering, compile
REQ-PLN-014	Wege, die ohne Zielsignal in sich zurückführen, und Fahrstraßen, die einen Abschnitt mehrfach befahren, sind Fehler.	H-004	loops_without_signal_are_rejected
REQ-PLN-015	Jede Fahrstraße mit Zielsignal erhält einen Durchrutschweg: ab dem Zielsignal bis zur ersten Grenze eines Gleisfreimeldeabschnitts hinter der Durchrutschweglänge (Vorgabe 100 m). Spitz befahrene Weichen im Durchrutschweg liegen im geraden Strang (ohne Angabe links). Endet die Fahrstraße an Netzgrenze oder Prellbock, gibt es keinen Durchrutschweg.	H-001, H-009	example_phase2_data
REQ-PLN-016	Für jede Weiche in Fahrweg und Durchrutschweg ist der nicht befahrene Strang geschützt: durch ein Signal, das auf die Weiche zu gerichtet ist (Haupt- oder Rangiersignal), oder durch eine Schutzweiche in abweisender Lage; spitz erreichte Weichen werden auf beiden Strängen bis zur Tiefe 16 weiterverfolgt, ein Prellbock schützt. Lässt sich ein Strang nicht schützen (Netzgrenze), ist das ein Projektierungsfehler. Jede Maßnahme ist dem Abschnitt zugeordnet, den sie schützt.	H-001	flanks_must_be_protectable, example_phase2_data
REQ-PLN-017	Jedes Vorsignal kündigt genau ein Hauptsignal an: das nächste in Wirkrichtung, ohne spitz befahrene Weiche dazwischen. Sonst ist das ein Projektierungsfehler.	H-009	distant_signals_need_a_unique_main_signal
REQ-PLN-018	Bahnübergänge im Fahrweg und im Durchrutschweg (innerhalb der Durchrutschweglänge) gehören zur Fahrstraße. Die Geschwindigkeit einer Fahrstraße ist die kleinste Geschwindigkeit der abzweigend befahrenen Weichen (ohne solche Weichen: Streckengeschwindigkeit).	H-010, H-002	example_phase2_data, level_crossing_within_long_overlap
REQ-PLN-019	Jeder Stellbereich wird für sich projektiert. Fahrstraßen können an einer Grenze enden. Je Grenze bestimmt die Projektierung den Annäherungsabschnitt (von der Grenze bis zum ersten nach innen gerichteten Hauptsignal, dem Einfahrsignal, samt dessen Durchrutschweg); vor dem Einfahrsignal liegt keine spitz befahrene Weiche. Ein Durchrutschweg darf keine Grenze überschreiten. Die Gegenprüfung leitet Grenzen und Annäherungsabschnitte unabhängig her. Format v3 enthält die Grenztabelle.	H-001, H-012	nordbahn_compiles_per_area, borders_need_an_entry_signal, inconsistent_border_data_is_rejected
REQ-PLN-020	Beim Laden wird ein Plan-Image abgewiesen, wenn zwei Fahrstraßen mit demselben Startsignal nicht als feindlich eingetragen sind (REQ-PLN-012, Regel 1). Darauf stützt sich die lineare Invariantenprüfung (REQ-IXL-023): Jede eingestellte Fahrstraße rechtfertigt höchstens ihr eigenes Startsignal.	H-007	inconsistent_phase2_data_is_rejected
REQ-PLN-021	Gekoppelte Weichen (REQ-TOP-017): Ein Weg, der gekoppelte Weichen gegen ihre Kopplung verlangt, ist keine Fahrstraße. Verlangt eine Fahrstraße eine gekoppelte Weiche in Fahr- oder Durchrutschweg, verlangt sie die Partnerweiche in der gekoppelten Lage als Flankenschutz; ebenso zu jeder gekoppelten Schutzweiche. Liegt eine so erzwungene Weiche zum Flankenweg hin, geht die Flankenschutzsuche über ihre Spitze hinaus weiter (z. B. über das zweite Zungenpaar einer DKW bis zum Signal vor dem anderen Ende). Gekoppelte Weichen im Annäherungsabschnitt einer Bereichsgrenze werden nicht projektiert. Das Plan-Image (v5) führt die Kopplung je Weiche; beim Laden wird es abgewiesen, wenn eine Kopplung nicht symmetrisch ist oder eine Fahrstraße bzw. ein Annäherungsabschnitt eine gekoppelte Weiche ohne ihre Partnerweiche in gekoppelter Lage verlangt. Die Gegenprüfung leitet Wege, Partner und Flankenschutz unabhängig aus einer Tabelle der zulässigen Lagenpaare her.	H-001, H-002, H-004	routes_over_a_double_slip_require_all_four_points, single_slip_has_one_curve, crossover_points_move_together, tampered_couplings_are_rejected, coupled_points_must_not_lie_in_an_approach, Szenario 25
REQ-PLN-022	Vier-Augen-Prinzip: Ein Plan kann von Prüfern freigegeben werden; eine Freigabe ist eine Ed25519-Signatur des Prüfers über einen Kontext und die Prüfsumme des Plans (getrennt von der Plansignatur). railit plan approve gibt erst nach Prüfung der Signatur des Erstellers und unabhängiger Gegenprüfung gegen das Netz frei. Mit --approvals N starten railitd und railit-node nur, wenn mindestens N verschiedene Prüfer aus --approver-key den Plan freigegeben haben; eine Freigabe des Erstellers, eines fremden Schlüssels oder zu einem anderen Plan weist den Plan ab.	H-008, H-004	plans_need_approvals_from_distinct_trusted_reviewers, plans_need_four_eyes_approval (railitd), keygen_compile_verify_info (CLI)