IBUK Libra

stawionokoncepcjęwirtualnegolaboratoriumCBAE,któregoprzeznaczeniem

jestbadanieiprzetwarzaniemodelirzeczywistychaplikacjiETCSwcelu:

−wsparciarozwoju/projektowaniaaplikacjiETCSpoprzeztestowanienowych

rozwiązańzwykorzystaniemwirtualnegoprototypowania,

−testowaniawłaściwościdynamicznychrzeczywistejaplikacjiETCSzwyko-

rzystaniemsymulacjideﬁniowanejprzezscenariuszeoperacyjne,

−odtwarzaniuzdarzeńhistorycznych.

Dwapierwszezastosowaniasąkluczowewkontekścieinnowacyjnegopodej-

ściadobadaniaaplikacjiETCSimająistotneznaczeniedlarozwojuwarsztatuna-

ukowegoprzestrzenibadawczejsystemuETCS.Pierwszeznich,wirtualneproto-

typowaniejestkoncepcją,któraumożliwiaznaczneprzyspieszenieprojektowania

aplikacjiETCSijejweryﬁkacjęwczasierzeczywistym.Drugiezastosowanieto

środowiskosymulacyjnewykorzystującegoscenariuszeoperacyjne.Scenariusze

operacyjnesąogólnieprzyjętymsposobemopisuoczekiwanegozachowaniasys-

temukolejowego(wszczególnościsystemuETCS),wokreślonychsytuacjach

ruchowych.Możliwośćsymulowaniarealizacjiscenariuszyoperacyjnychprzy

różnychwarunkachpoczątkowychjestkluczemdopełnejweryﬁkacjipoprawno-

ściaplikacjiETCS.Piątyrozdziałtoczęśćmonograﬁiopisującaaparatmatema-

tycznystanowiącypodstawyteoretyczneCyfrowegoBliźniakaAplikacjiETCS.

Zawieraonzbiórmodeliialgorytmów,któremajązastosowaniedlarealizacji

precyzyjnego,cyfrowegoodwzorowaniaaplikacjiETCS.Wrozdzialetymwpro-

wadzonyzostałmatematycznyaparatwpostaciMultigrafuIS,którywszechstron-

nieodwzorowujestrukturyinfrastrukturykolejowej,łączącwsobiemodele:to-

pologiiukładutorowego,infrastrukturyfunkcjonalnejwarstwypodstawowejoraz

aplikacjiETCS.Uzupełnieniemjestmodelformalnyscenariuszaoperacyjnego.

Wdalszejczęścirozdziałupiątegowprowadzonychjestkilkamodeliskupiają-

cychsięnamodelachformalnychpociąguorazprocesujazdy.Modeletedalej

sąprzedstawionejakospójneśrodowiskosymulacjiscenariuszyoperacyjnych,

którestanowiąnarzędziedoweryﬁkacjipoprawnościaplikacjiETCS.Wostatnim

punkcietegorozdziałuwprowadzonyzostajejeszczejedenmodelaplikacjiETCS

wykorzystującyautomatywspółbieżneIMDS.Jesttoprzykładzastosowaniame-

todformalnychdlaweryﬁkacjiwybranychcechaplikacjiETCSzapomocąwery-

ﬁkacjimodelowej.Weryﬁkacjamodelowaniesprawdzakonkretnychprzebiegów

systemu,leczanalizujeje„wszystkierazem”,dającformalnydowódspełnienia

lubniespełnieniaokreślonychwłasności.Jesttocecha,któradajeznaczącąprze-

wagętemupodejściunadrozwiązaniamisymulacyjnymi.Zastosowanyforma-

lizmzostałopracowanywInstytucieInformatykiPolitechnikiWarszawskiej.Jest

tospecjalizowanenarzędziedomodelowaniaasynchronicznych,rozproszonych

systemówwspółbieżnychpowalającenabadanietakichzjawiskjakzakleszcze-

nieczyzagłodzenieautomatumodelującegosystem.Monograﬁękończypodsu-

mowanie,wktórymrozważaniapoddanezostałydotychczasoweefektypracy

Brak wyników