z. 95 Transport 2013
Piotr Kawalec
Politechnika Warszawska, Wydzia Transportu
Marcin Rysko
Bombardier Transportation (Rail Engineering) Polska sp. z o.o.
ZASTOSOWANIE
GRAFÓW
PRZEJ
AUTOMATÓW
SKO CZONYCH
DO
OPISU
ALGORYTMÓW
DZIAANIA
URZDZE
SRK
Rkopis dostarczono, kwiecie 2013
Streszczenie: W artykule przedstawiono propozycj stworzenia metody formalnego zapisu
algorytmów dziaania urzdze zabezpieczenia ruchu kolejowego z wykorzystaniem grafów przej automatów skoczonych. Przegld stosowanych obecnie metod opisu urzdze srk wskazuje, e nie istnieje jednolita platforma opisu wszelkiego rodzaju dyskretnych ukadów sterowania. Wikszo stosowanych metod nie pozwala na wykorzystanie wspomagania komputerowego na etapie specyfikacji i weryfikacji tego typu ukadów. Na przykadzie stworzonego modelu przykadowego urzdzenia zostao pokazane, e zastosowanie do tego celu grafów przej pozwala stworzy kompletn platform specyfikacji algorytmów dziaania urzdze srk, pozwalajc dodatkowo na statyczn i dynamiczn weryfikacj poprawnoci opisu z wykorzystaniem jzyków opisu sprztu.
Sowa kluczowe: automat skoczony, system zalenociowy, sterowanie ruchem kolejowym
1. WSTP
Wraz z nieustajcym wzrostem zoonoci urzdze i systemów sterowania ruchem kolejowym oraz zwikszajc si liczb realizowanych przez nie funkcji narastaj trudnoci z opisem dziaania tych ukadów na poziomie algorytmów. Systemy srk nale do tej grupy urzdze automatyki, w której warunki dotyczce bezpieczestwa i niezawodnoci dziaania s najbardziej restrykcyjne. Kady bd w ich funkcjonowaniu moe potencjalnie prowadzi do zagroenia ycia ludzkiego i wysokich strat materialnych. Dlatego coraz wiksz wag przykada si do formalnych metod opisu tych urzdze. Prowadzone s prace badawcze ukierunkowane na formalne metody specyfikacji urzdze sterowania ruchem kolejowym [4, 6, 8, 9]. Tworzone s równie specjalne jzyki programowania dedykowane wycznie projektowaniu takich ukadów [3].
Artyku przedstawia koncepcj stworzenia metody projektowania z wykorzystaniem grafów przej automatów skoczonych oraz opisuje moliwoci formalnej weryfikacji grafów pry pomocy jzyków opisu sprztu. Zaprezentowany zosta proces budowy algorytmu dziaania dla przykadowego urzdzenia sterowania ruchem kolejowym oraz moliwoci weryfikacji tego algorytmu z wykorzystaniem jzyków opisu sprztu.
2.METODY PROJEKTOWANIA STACYJNYCH
URZDZE SRK
W urzdzeniach mechanicznych, elektromechanicznych oraz pierwszych rozwizaniach przeka nikowych obwody elektryczne projektowane byy indywidualnie. Dla tego typu systemów istniay albumy schematów, przedstawiajce wybrane przypadki projektowe, w aden sposób nie dao si jednak bezporednio wykorzysta elementów do nowego projektu. Prace projektowe opieray si na tworzeniu obwodów przez analogi do zaprezentowanych przykadów [14].
W latach 60-tych rozpoczto wdraanie na sieci PKP systemu PB opartego o uprzednio przygotowane szablony zwane blankietami. O ile w warstwie projektowej korzystanie z gotowych schematów blankietowych istotnie uatwiao tworzenie czci obwodów, fizycznie urzdzenia te nadal budowane byy z pojedynczych przeka ników [10].
Znaczc zmian przynioso wprowadzenie urzdze o strukturze zblokowanej. Istot tego podejcia by podzia elementów infrastruktury srk na podstawowe elementy (takie jak semafor, zwrotnica), zidentyfikowanie uniwersalnego sposobu dziaania kadego elementu, stypizowanie rozwiza dla kadego moduu, a nastpnie wykorzystywanie przygotowanych, uniwersalnych moduów do tworzenia projektów dla zadanych ukadów torowych. Pierwszym systemem o cakowicie zblokowanej strukturze, który zosta wdroony na sieci PKP by system IZH-111. W urzdzeniach tych moduami okrelane byy zestawy przeka nikowe odpowiadajce urzdzeniom zewntrznym, czone kablami
geograficznymi zgodnie z ukadem torowym [11].
Równie w obecnie wdraanych komputerowych systemach zalenociowych korzysta si z idei urzdze geograficznych na etapie tworzenia aplikacji. W takich systemach pod pojciem moduu rozumie si zbiory równa zalenociowych specyficznych dla danego elementu sterowanego. Topologia stacji (powizania geograficzne pomidzy moduami) wprowadzana jest do systemu na etapie projektowania i na jej podstawie komputer zalenociowy realizuje zadane funkcje [2].
Koncepcja urzdze zblokowanych jest stale uywana i rozwijana, niezalenie od techniki realizacji urzdze. Brakuje jednak sformalizowanej metody tworzenia algorytmów tego typu ukadów, która pozwoliaby na unifikacj sposobu realizowania funkcji zalenociowych i uproszczenie tworzenia powiza pomidzy systemami. Wykorzystywane metody projektowania to w wikszoci metody heurystyczne,
nie pozwalajce na jednoznaczne stwierdzenie, e opracowany algorytm dziaania
Widoczny jest brak jednego, kompletnego rodowiska, w którym proces projektowania byby pozbawiony wymienionych niedogodnoci.
3. METODA TWORZENIA ALGORYTMÓW URZDZE
ZALE NO CIOWYCH
Przedstawiona w niniejszym artykule metoda opisu dziaania urzdze srk stanowi prób stworzenia jasnych, sformalizowanych zasad budowy algorytmów tego typu ukadów, wykorzystujc do tego grafy przej automatów skoczonych. Formalizacja podejcia wymuszona jest wysokim stopniem zoonoci realizowanych funkcji, co sprawia, e tworzenie specyfikacji metodami heurystycznymi jest niezwykle utrudnione.
Podstawowym zaoeniem wykorzystywanym przy modelowaniu stacyjnych urzdze sterowania ruchem kolejowym jest to, e s to urzdzenia pracujce sekwencyjnie. Na podstawie analizy sposobu dziaania istniejcych na sieci PKP stacyjnych urzdze srk zaproponowany zosta podzia pracy urzdze na charakterystyczne fazy. W pierwszym etapie nastpuje wybór drogi przebiegu, która okrelona jest przez sygnalizator pocztkowy i kocowy. Nastpnie przebieg jest nastawiany (zwrotnice wysterowywane s do danych pooe) i gdy droga przebiegu zostaa poprawnie uoona, nastpuje utwierdzenie przebiegu (oraz wywietlenie sygnau zezwalajcego). Ostatnim etapem jest zwolnienie przebiegu, po którym ukad wraca do stanu spoczynkowego i jest gotowy do przyjcia kolejnych polece. Schematycznie cykl ten przedstawiony zosta na rys. 1. Liczba moliwych do zrealizowania przebiegów p oznaczona zostaa jako P.
Rys. 1. Cykl pracy stacyjnych urzdze zalenociowych
W przypadku urzdze niegeograficznych, powyszy schemat nie nadaje si do opisu pracy caego systemu. Pomijajc trudno wynikajc z duej liczby moliwych
...
...
...
przebiegów, cz z nich moe by realizowana jednoczenie, czego taki model nie zakada.
Przyjmujc jednak filozofi urzdze zblokowanych zaoono, e przedstawiony cykl pracy odnosi si do jednego elementu urzdze stacyjnych. W odniesieniu do pojedynczego moduu przebieg rozumiany jest jako moliwo wykorzystania danego elementu w drodze jazdy. Naturalnie w danym cyklu pracy realizowany moe by tylko jeden przebieg.
Po dokonaniu sownego opisu dziaania zgodnego z zaproponowanym schematem konieczne jest sformalizowanie zapisu. Wykorzystano do tego celu logiczny schemat algorytmu [1, 13]. Zgodnie z opisanymi zaoeniami oraz zasadami tworzenia logicznych schematów algorytmów (LSA), wykonany zosta formalny zapis podstawowego algorytmu dziaania elementu systemu geograficznego, który przedstawiono poniej.
0 11 21 1 0 1 2 11 12 11 21 22 21 1 2 1 1 1 2 2 12 13 12 22 23 22 2 3 2 1 1 2 2 13 14 13 23 24 23 3 4 3 1 1 2 2 14 1 ... ... ... ... P swP S sw sw P P P WP wnP W wn W wn P P P NP nuP N nu N nu P P P UP uzP U uz U uz Z Y X X X Y X Y X Y X Y X Y X Y X Y X Y X Y X Y X
Z
Z
Z
Z
Z
Z
Z
Z
Z
Z
p n n n n p n np n n p n n p n np n n p n n p n np n n p n n p 10 14 24 2 20 24... 4 0 4 P P ZP zsP zs n npZ
Y XZ zs n n pZ
Y X n nZ
Przyjto nastpujce oznaczenia:
Ymp - symbol wektora zmiennych wyjciowych w stanie m w przebiegu p,
Xmnp - symbol wektora zmiennych wejciowych, bdcego warunkiem przejcia ze
stanu m do stanu n w przebiegu p.
Na podstawie tak wykonanego zapisu w prosty sposób moliwa jest budowa grafu przej automatu skoczonego. Dla kadego symbolu wektora zmiennych wyjciowych naley utworzy stan o wartoci zmiennych wyjciowych zgodnie z wartoci wektora. Stany musz by nastpnie poczone tranzycjami o warunkach przejcia opisanych w LSA. W wyniku powyszych przeksztace powsta graf przej , który przedstawiono na rys. 2.
Okrelenie wymaganej dla danego elementu liczby moliwych do realizacji przebiegów (P) oraz zidentyfikowanie warunków wykonania poszczególnych tranzycji (X...) pozwala na uzyskanie kompletnego opisu dziaania zadanego elementu. Zastosowanie automatu skoczonego do opisu stworzonego algorytmu ma kilka zasadniczych zalet. W naturalny sposób wykluczone s sprzeczne dziaania ukadu (na przykad jednoczesne wybieranie przebiegu 1 i utwierdzanie w przebiegu 2), poniewa automat w danej chwili moe znajdowa si tylko w jednym stanie. Ponadto wyeksponowanie tranzycji uniemoliwia specyfikowanie nieprawidowych przej (na przykad przejcie ze stanu nastawiania przebiegu 1 do stanu utwierdzenia przebiegu 2).
Rys. 2. Ogólna posta grafu przej dla elementu systemu geograficznego
Wykonany graf przej moe zosta nastpnie wykorzystany do wykonania specyfikacji algorytmu w jzyku VHDL. Jest to jeden z najpopularniejszych obecnie jzyków opisu sprztu [5, 7, 12]. Konieczny jest do tego pakiet posiadajcy edytor umoliwiajcy generowanie kodu jzyka na podstawie grafu. Takim rodowiskiem jest na przykad wykorzystany tutaj pakiet Active-HDL firmy Aldec wyposaony w edytor grafów przej FSM. Moliwoci specyfikacji oraz weryfikacji grafu przej stworzonego wedug opisanej metody pokazane zostan na przykadowym algorytmie opracowanym dla moduu logicznego zwrotnicy.
Zwrotnic w drodze jazdy wykorzysta mona w czterech kierunkach, std liczba przebiegów P dla tego moduu wynosi 4. Nazewnictwo przebiegów odpowiada moliwociom przejazdu po zwrotnicy, zgodnie z rys. 3.
Po zadeklarowaniu zmiennych wejciowych i wyjciowych oraz okreleniu warunków logicznych dla tranzycji pomidzy poszczególnymi stanami stworzony zosta graf przej , którego specyfikacja w edytorze FSM przedstawiona zostaa na rys. 4.
Rys. 4. Graf przej dla moduu zwrotnicy w edytorze FSM
Dziki wykorzystaniu grafu przej i edytora FSM nie jest konieczne tworzenie kodu jzyka VHDL od podstaw, jego struktura zostanie wygenerowana automatycznie na podstawie deklaracji i warunków ujtych na opracowanym grafie. Tak wykonana specyfikacja moe posuy nie tylko do syntezy i wykonania prototypu ukadu, ale take do formalnej weryfikacji modelu, co opisane zostanie w kolejnym rozdziale.
4. WERYFIKACJA
ALGORYTMU
Z
WYKORZYSTANIEM
WSPOMAGANIA
KOMPUTEROWEGO
Przeprowadzenie weryfikacji oraz symulacji dziaania zaprojektowanego algorytmu moliwe jest dziki zastosowaniu symulatora logicznego, bdcego skadnikiem pakietu Active-HDL. Symulacja dziaania polega na przypisaniu wymusze do zmiennych wejciowych i badaniu odpowiedzi ukadu. Wymuszeniami mog by na przykad zegary predefiniowane, sygnay losowe lub klawisze Hotkey. Prac modelu podczas symulacji obserwowa mona bezporednio na grafach i schematach blokowych (graficznie) oraz na przebiegach symulacji. Przebiegi czasowe symulacji umoliwiaj rejestrowanie stanu kadej zmiennej w dowolnie wybranej chwili. Poniewa w miar rozbudowy ukadu weryfikacja wykonywana rcznie byaby coraz trudniejsza, pakiet Active-HDL umoliwia wygenerowanie sekwencji wymusze, która pozwala sprawdzenie wszystkich tranzycji i wartoci zmiennych wyjciowych. Rys. 5 przedstawia przebiegi symulacji podczas weryfikacji.
Rys. 5. Zapis automatycznej weryfikacji
Na rys. 6 pokazano moliwo obserwacji zachowania ukadu opisanego grafem bezporednio w edytorze FSM. Stan, w którym obecnie znajduje si element wyróniony jest kolorem ótym.
Rys. 6. Podgld symulacji w edytorze FSM
Weryfikacja umoliwia sprawdzenie, czy przejcia pomidzy stanami zachodz przy zgodnych z projektem wartociach zmiennych wejciowych, oraz czy wartoci zmiennych wyjciowych w kadym ze stanów odpowiadaj zaprojektowanym w algorytmie. Ten etap projektowania pozwala wyeliminowa bdy przypadkowe powstae przy tworzeniu specyfikacji. Pozytywny wynik weryfikacji modelu moe stanowi punkt wyjcia do dalszych bada nad poprawnoci projektu. Aby umoliwi symulacj algorytmu w powizaniu z innymi elementami, skorzystano z edytora schematów blokowych BDE. W tym edytorze specyfikacja wykonana jako graf przej przedstawiona jest jako blok, do którego wprowadzi mona sygnay z innych bloków lub wej . Moliwo tworzenia rozbudowanych struktur hierarchicznych jest niezwykle pomocn cech w przypadku analizy pracy stacyjnych systemów zalenociowych.
Rys. 7 przedstawia wyspecyfikowany blok odwzorowujcy modu zwrotnicy
w otoczeniu ssiadujcych elementów geograficznych. Po zbudowaniu algorytmów
niezbdnych elementów stacyjnych urzdze srk moliwe bdzie zweryfikowanie wszystkich zalenoci, symulujc wspódziaanie algorytmów w edytorze BDE.
Poniewa wszystkie opisane etapy specyfikacji oraz symulacji wykonywane s w jednym rodowisku wspomagania komputerowego, kada nieprawidowo w specyfikacji moe by niezwocznie poprawiona bez potrzeby zmiany platformy projektowania. Zastosowanie omawianego rodowiska projektowego stanowi wic kompletn platform projektow, pozwalajc na wykonanie wszystkich etapów tworzenia specyfikacji ukadu.
6. PODSUMOWANIE
Metoda budowy algorytmów urzdze srk przedstawiona w artykule pozwala
w jednoznaczny sposób przej od opisu sownego do grafu przej automatu
skoczonego. Zapis w takiej postaci stanowi dogodn podstaw zarówno do stworzenia penej specyfikacji w kodzie jzyka opisu sprztu, jak i do przeprowadzenia symulacji dziaania obiektu z wykorzystaniem symulatorów logicznych. Rozwinicie metody o specyficzne funkcje poszczególnych urzdze (takie jak zapewnianie ochrony bocznej czy dora ne zwolnienie przebiegu) oraz zastosowanie jej do wszystkich elementów stacyjnych urzdze srk moe stanowi podstaw do stworzenia penego, formalnego opisu dziaania systemu zalenociowego.
Bibliografia
1. Apuniewicz S.: Ukady przeka nikowe w automatyce zabezpieczenia ruchu kolejowego. WPW, Warszawa 1969.
2. Dbrowa-Bajon M.: Podstawy sterowania ruchem kolejowym. OWPW, Warszawa 2007.
3. Fokkink W., Groote J., Hollenberg M., van Vlijmen B.: LARIS 1.0 Language for Railway Interlocking Specifications. CWI, 2000.
4. Hlavatý T., Peuil L., Štpán P.: Case Study: Formal Methods in Development and Testing of Safety Critical Systems: Railway Interlocking System. EUROMICRO 2001.
5. Kalisz J. (red.): Jzyk VHDL w praktyce. WKi, Warszawa 2002.
6. Kanso K., Moller F., Setzer A.: Automated Verification of Signaling Principles in Railway Interlocking Systems. Eighth International Workshop of Automated Verification of Critical Systems, Glasgow 2008. 7. Kawalec P., Koliski D.: Modelowanie interlocking'u z zastosowaniem jzyka opisu sprztu. Logistyka
6/2010, Instytut Logistyki i Magazynowania, Pozna, 2010, str. 1329 – 1337.
8. Kawalec P., Rysko M.: Komputerowo wspomagana specyfikacja funkcji zalenociowych urzdze srk. Technika Transportu Szynowego TTS 9/2012, ód , 2012, str. 1605 – 1614.
9. Kawalec P., Rysko M.: Zastosowanie jzyków opisu sprztu do specyfikacji urzdze srk. Logistyka 4/2012, Pozna, 2012, str. 351 – 358.
10. Mickiewicz T., Zubkow A.: Przeka nikowe urzdzenia nastawcze typu póblokowego. WKi, Warszawa 1961.
11. Miksza E., Olendrzyski W., Zubkow A.: Zblokowany system sterowania ruchem kolejowym na stacjach typu IZH 111. WKi, Warszawa 1979.
12. Pasierbiski J., Zbysiski P.: Ukady programowalne w praktyce. WKi, Warszawa 2002. 13. TraczykW.: Ukady cyfrowe. Podstawy teoretyczne i metody syntezy. WNT, Warszawa 1982.
14. Zajczkowski A., Kaliciska K., Olendrzyski W.: Elektryczne urzdzenia zabezpieczenia ruchu kolejowego. Urzdzenia stacyjne. WKi, Warszawa 1976.
RAILWAYINTERLOCKINGALGORITHMSCONSTRUCTION
USINGFINITE-STATEMACHINEDIAGRAMS
Summary: The article presents a method of railway traffic control algorithm specification using finite-state
machine diagrams. The review of currently used description methods of railway traffic control devices and systems indicates that a complete platform for description of all kinds of discrete control systems does not exist. It is shown that application of FSM diagrams for this purpose comprises a uniform platform for specification and verification of railway traffic control devices, which additionally allows static and dynamic verification of correctness of this description with the use of hardware description languages and logic simulators. On the exemplary operation algorithm of point module, both the possibilities of Active–HDL package as well as the process of computer aided specification and verification of the designed system are presented.