1.1.Cyfrowe odwzorowanie aplikacji ETCS. Dorobek badawczy 1.2.Plan monografii 1.3.Aktualny stan wiedzy 1.3.1.Cyfrowy bliźniak 1.3.2.Modelowanie i formalny opis systemu srk 1.3.3.Weryfikacja poprawności modelu infrastruktury 1.3.4.Metody formalne w zastosowaniu do weryfikacji systemu ETCS 2.System ERTMS/ETCS i jego aplikacja 2.1.System ERTMS 2.1.1.Kluczowe funkcje 2.1.2.Składniki i struktura 2.1.3.Poziomy zastosowania 2.1.4.Tryby pracy 2.1.5.Procedury 2.1.6.Język ETCS 2.2.Aplikacja ETCS 2.3.Formalne podstawy stosowania scenariuszy operacyjnych w procesie weryfikacji poprawności aplikacji ETCS 3.Cyfrowy bliźniak 3.1.Koncepcja 3.2.Właściwości 3.3.Zastosowania 4.Cyfrowy bliźniak aplikacji ETCS 4.1.Koncepcja 4.1.1.Cyfrowy bliźniak 4.1.2.Interfejs fizycznego bliźniaka 4.1.3.Monitor AE 4.1.4.60Archiwum 4.1.5.Interfejs operatora/konsola operatora 4.1.6.Wirtualne laboratorium 4.2.Taksonomia 4.3.Zastosowanie 4.4.Identyfikacja modeli składowych CBAE 4.4.1.Ogólny zarys modelu 4.4.2.Pozycjonowani 4.4.3.Model topologii układu torowego 4.4.4.Modele składników aplikacji ETCS 4.4.5.Modelowanie aplikacji ETCS 4.4.6.Modele elementów otoczenia aplikacji ETCS 4.4.7.Modelowanie otoczenia 4.4.8.Model CBAE 4.5.Wirtualne laboratorium aplikacji ETCS 4.5.1.Założenia 4.5.2.Wirtualne prototypowanie 4.5.3.Koncepcja wirtualnego prototypu aplikacji ETCS 4.5.4.Symulacja scenariuszy operacyjnych 4.6.Dynamiczny model pociągu 4.6.1.Fazy jazdy pociągu 4.6.2.Strategia jazdy pociągu 4.6.3.Równanie ruchu 4.6.4.Interpolacja siły trakcyjnej i hamowania 4.6.5.Dokładność modelu jazdy 4.7.Symulacja jazdy pociągu 4.7.1.Zarys algorytmu 4.7.2.Algorytm symulacji jazdy pociągu 4.7.3.Algorytm symulacji ruchu kolejowego 4.7.4.Modele matematyczne i algorytmy 5.1.Podstawy teoretyczne 5.2.Matematyczny model infrastruktury torowej obejmującej aplikację ETCS i jej otoczenie 5.2.1.Multigraf infrastruktury kolejowej 5.2.2.Katalog wierzchołków i krawędzi Multigrafu IS 5.2.3.Model przykładowego obszaru sieci kolejowej 5.3.Algorytmy weryfikacji poprawności modelu struktury 5.3.1.Ogólne założenia 5.3.2.Obszary weryfikacji 5.3.3.Spójność modelu matematycznego163 5.3.4.Właściwości warstwy podstawowej srk 5.3.5.Budowa aplikacji ETCS 5.4.Scenariusze operacyjne 5.4.1.Formalna specyfikacja 5.4.2.Specyfikacja SSO środowiska symulacji 5.4.3.Wykonanie badania symulacyjnego 5.4.4.Weryfikacja działania aplikacji ETCS 5.4.5.Graficzna reprezentacja scenariusza operacyjnego 5.5.Formalna weryfikacja cyfrowego bliźniaka aplikacji ETCS z wykorzystaniem modelu czasowego i współbieżnego 5.5.1.Rozproszony charakter aplikacji ETCS 5.5.2.Dobór narzędzia 5.5.3.IMDS 5.5.4.Weryfikacja dostępność komunikatów tekstowych na DMI