Formalny opis funkcji zależnościowych systemów srk dla wspóczesnych posterunków ruchu Formal Description of Interlocking Functions of Railway Traffic Control Systems

Pełen tekst

(1)PRACE NAUKOWE POLITECHNIKI WARSZAWSKIEJ z. 86. Transport. 2012. Dariusz Koli ski Egis Poland sp. z o.o.. FORMALNY OPIS FUNKCJI ZALENO CIOWYCH SYSTEMÓW SRK DLA WSPÓCZESNYCH POSTERUNKÓW RUCHU R kopis dostarczono, czerwiec 2012. Streszczenie: W artykule podj to prób opracowania formalnego opisu funkcji zalenociowych. Wychodzc z odwzorowania systemu zalenociowego w postaci obiektów, zaproponowano formalny opis funkcji zalenociowych, obiektów tworzonych z opracowanych funkcji oraz opis systemu zalenociowego tworzonego z obiektów. Zastosowanie elementów teorii grafów, automatów, zbiorów pozwolio na opracowanie opisu formalnego, umoliwiajcego opis funkcji zalenociowych. Sowa kluczowe: sterowanie ruchem kolejowym, system zalenociowy, formalizacja opisu. 1. WSTP Podstaw bezpieczestwa ruchu pocigów s cechy funkcjonalne (funkcjonalnoci) implementowane w urzdzeniach sterowania ruchem kolejowym (srk) oraz przestrzeganie procedur przez personel uczestniczcy w prowadzeniu ruchu pocigów. Zastosowanie techniki mikroprocesorowej do realizacji zalenoci w systemach srk nie zostao poprzedzone ogólnodost pnymi pracami koncepcyjnymi dotyczcymi przeniesienia funkcjonalnoci stosowanych w systemach realizowanych w technice przeka nikowej do systemów mikroprocesorowych. Producenci niezalenie od siebie i zachowujc tajemnic przed konkurencj poszukiwali wasnych rozwiza. W efekcie powstaway dwa gówne nurty projektowania systemów zalenociowych. W pierwszym z nich wartoci funkcji wyj

(2) systemu zalenociowego wyznaczane s w oparciu o wyniki z rozwiza równa zalenociowych. W drugim wartoci funkcji wyj

(3) systemu zalenociowego odczytywane s z zapisanych w pami ciach danych (mapowanie wyj

(4) ). Konsekwencj takiego podejcia u podstaw tworzenia pierwszych mikroprocesorowych systemów srk bya konieczno

(5) specyficznego i indywidualnego poszukiwania form opisu funkcji zalenociowych. Kady z producentów stan przed problemem wytworzenia specjalistycznego oprogramowania narz dziowego dla opracowanego systemu. Natomiast producenci sterowników PLC (ang. Programmable Logic Controller) znajc powszechne przywizanie do wszechobecnych wówczas w sterowaniu przeka ników.

(6) 36. Dariusz Koliski. opracowali j zyki schematów przeka nikowych, nazywanych równie j zykami logiki drabinkowej (np. Grafcet, LAD ang. Ladder Logic) [19]. W efekcie doszo do swoistej izolacji wiedzy a prace badawcze skoncentroway si na modelowaniu elementów skadowych systemów srk. Zabrako prac dotyczcych formalizacji opisu funkcji zalenociowych a jedyn paszczyzn opisu pozosta opis behawioralny. Opracowana metoda opisu funkcji zalenociowych na podstawie dost pnych opisów behawioralnych nie determinuje technologii ich realizacji.. 2. OGÓLNE ZAOENIA FORMALIZACJI OPISU SYSTEMU SRK DLA POSTERUNKU RUCHU W systemie srk kadego posterunku ruchu (rys.2.1.) wyst puj trzy warstwy: nadrz

(7) dna (górna zakreskowana na rysunku), zale no ciowa (rodkowa) i wykonawcza (dolna zakropkowana). Warstwa nadrz dna odpowiada za realizacje funkcji zwizanych z archiwizacj zdarze dotyczcych ruchu pocigów, stanu obiektów sterowanych i zdarze awaryjnych, zobrazowanie stanu obiektów systemu oraz wprowadzanie polece nastawczych. Warstwa zalenociowa jest obszarem wyst powania funkcji zalenociowych. W niej sprawdzane s warunki umoliwiajce proces wysterowania obiektów warstwy wykonawczej. Proces ten obejmuje cig kontrol stanu urzdze i sytuacji ruchowej na posterunku ruchu oraz generowanie polece sterujcych do warstwy wykonawczej, jak równie generowanie informacji o stanie obiektów do warstwy nadrz dnej. Proces ten jest nazywany realizacj zalenoci (uzalenie). Pod poj ciem zalenoci naley rozumie

(8) zbiór wymaga definiujcych pr dko

(9) jazdy wedug cile ustalonych zasad wynikajcych z wyznaczonej drogi jazdy oraz istniejcej sytuacji ruchowej. W niniejszej pracy zbiór wymaga i sposób ich realizacji w warstwie zalenociowej nazywany b dzie dalej funkcjami zalenociowymi. Warstwa wykonawcza odpowiada za bezporedni kontrol stanu obiektu warstwy wykonawczej oraz waciwe wysterowanie tego obiektu po otrzymaniu polecenia z warstwy zalenociowej. Kada z warstw systemu srk ma wasne wymagania dotyczce realizowanych funkcji a pomi dzy warstwami odbywa si wymiana informacji za pomoc ukadów sekwencyjnej transmisji. Prezentowane zagadnienie opisu funkcji zalenociowych dotyczy warstwy zalenociowej (rodkowej). Dla mikroprocesorowych urzdze srk przygotowywane s trzy gówne dokumenty dotyczce realizacji zalenoci na posterunku ruchu kolejowego. S to: plan schematyczny, schemat powiza ukadu torowego i obiektów oraz tablica zalenoci. Tablica zalenoci definiuje podane pooenia obiektów srk w drodze jazdy, drodze ochronnej i ochronie bocznej dla projektowanych przebiegów. Ponadto okrela ona moliwo

(10) wspórealizacji przebiegów oraz okrela pr dkoci jazdy pocigów dla kadego przebiegu. Plan schematyczny ilustruj rozmieszczenie urzdze srk naniesione na uproszczonym ukadzie torowym..

(11) Formalny opis funkcji zalenociowych systemów srk dla wspóczesnych …. Ukad wprowadzania polece. Automatyczne. Przebiegowe. Indywidualne. Sterowanie. 37. Nastawnia Ukady diagnostyki urzdze srk. Rozkad jazdy. Ukad zobrazowania i rejestracji zdarze. „Czarna skrzynka”. Obiekty. System zale no ciowy. Poczenia transmisyjne. Komparatory bezpieczne (Interfejsy sterowania urzdzeniami w terenie). Obiekty. Poczenia transmisyjne. Rys. 2.1. Schemat warstwowy systemu sterowania ruchem kolejowym. Schemat powiza ukadu torowego i obiektów ilustruje ich ssiedztwo w terenie oraz symboliczne powizania. Pod poj ciem obiektu (w warstwie zalenociowej) naley rozumie

(12) logiczne odwzorowanie elementów ukadu torowego lub obiektów planu schematycznego takich jak: odcinki torowe, rozjazdy, sygnalizatory, przejazd i blokada.

(13) 38. Dariusz Koliski. liniowa. Sposób zobrazowania obiektów i ich symboliczny opis zosta zaproponowany w pracy [23]. Z uwagi na nieco inny zbiór obiektów stosowany w niniejszej pracy zdefiniowano go w (3.1) i zobrazowano na rysunku 2.2.. Rys. 2.2. Piktogramy odwzorowujce obiekty w systemie srk. Poszczególne symbole opisu w piktogramach obiektów oznaczaj: J - odcinek torowy krótki, L - odcinek torowy dugi, T - skrzyowanie torów, Z - rozjazd zwyczajny, K - rozjazd krzyowy, W - wykolejnica, S - semafor, M - tarcza manewrowa, B - blokada liniowa, P - przejazd. NO - nazwa wasna obiektu (z planu schematycznego), Nr O - numer obiektu w posterunku ruchu, J nr – numer obiektu typu J, 1-4 strony obiektu. aden z wymienionych powyej dokumentów nie definiuje sposobu wysterowania poszczególnych obiektów do podanych pooe. Poniewa nie istnieje jeden dokument, który opisywaby warunki zalenociowe, zatem do ich opis w postaci funkcji zalenociowych opracowany zosta z zastosowaniem obowizujcych przepisów, literatury fachowej [2, 3, 4, 23] oraz dowiadczenia autora [8, 9, 10, 11, 12, 13, 15]. Podjecie zagadnienia formalizacji opisu funkcji zalenociowych wymagao przygotowania opisu behawioralnego tych funkcji, jako podstawy rozpocz cia formalizacji. Z uwagi na obj to

(14) niniejszej pracy opisy behawioralne nie zostay zamieszczone. W rzeczywistych systemach srk wyst puj obiekty tego samego rodzaju o rónych cechach funkcjonalnych np.: x semafory: wjazdowe, wyjazdowe i drogowskazowe, x rozjazdy krzyowe: pojedyncze i podwójne, x blokady liniowe: pósamoczynne i samoczynne. Przyj to zaoenie, e kady rodzaj obiektu z wyej wymienionych b dzie opracowywany uniwersalnie, tak aby umoliwia odwzorowywanie wszystkich cech funkcjonalnych. Wanym poj ciem w procesie sterowania urzdzeniami srk jest utwierdzenie, które oznacza zachowanie pooe elementów przebiegu (drogi jazdy, drogi ochronnej i ochrony bocznej) wymaganych dla jazdy taboru do czasu, gdy jazda ta si odb dzie, bd nastpi.

(15) Formalny opis funkcji zalenociowych systemów srk dla wspóczesnych …. 39. uchylenie stanu utwierdzenia przebiegu poleceniem specjalnym wprowadzonym przez obsug . Dotychczas stosowano utwierdzanie wszystkich elementów przebiegu lub utwierdzenie tzw. sekcji, oznaczajcych kolejne niezalene fragmenty przebiegu. Ze wzgl du na rodzaj rozróniamy utwierdzenia pocigowe (U) i manewrowe (Um). W pracy zaproponowano indywidualne utwierdzane obiektów w przebiegu na zasadach obowizujcych dla sekcji, z jednoczesnym wprowadzeniem nowego poj cia „utwierdzenia kierunkowego”. Definicja 1 Utwierdzenie kierunkowe jest to utwierdzenie obiektu z dokadno ci do jego rodzaju, kierunku i zwrotu jazdy taboru. Dotyczy ono obiektów takich jak odcinki torowe, rozjazdy, wykolejnica, przejazd. Oznacza to, e odcinek torowy b dzie mia 2 utwierdzenia kierunkowe dla jazd pocigowych (Upoc12, Upoc21) i 2 dla jazd manewrowych, (Uman12, Uman21). Skrzyowanie torów b dzie miao odpowiednio po 4 takie utwierdzenia, a rozjazd krzyowy b dzie mia 8 utwierdze pocigowych i 8 utwierdze manewrowych. Wprowadzenie poj cia utwierdze kierunkowych w znakomity sposób eliminuje ilo

(16) wyklucze specjalnych jaka wyst puje w tablicy zalenoci. Dotychczasowe próby przedstawienia w postaci jednego grafu cho

(17) by najprostszego obiektu srk pokazay, e jest to problemem klasy problemów NP-trudnych, albowiem zoono

(18) algorytmów sterowania ronie wykadniczo (2n) w zalenoci od iloci zmiennych wejciowych. Zatem, nawet dla niewielkich iloci zmiennych wejciowych niewykonalne jest opracowanie grafu odpowiadajcego obiektowi. Skoro nie mona opracowa

(19) grafu obiektu, to nie mona opracowa

(20) formalnej metody dekompozycji grafu obiektu na podgrafy [18]. Natomiast moliwy jest podzia logiczny obiektu na cz ci w taki sposób, aby kadej z cz ci odpowiadaa jedna funkcja zalenociowa sporód realizowanych przez obiekt. Funkcja ta moe by

(21) odzwierciedlona w postaci grafu, bo posiada znacznie mniej zmiennych wejciowych. Tak rozumiany podzia b dzie w dalszej cz ci pracy nazywany dekompozycj na funkcje zalenociowe. Dekompozycja ta wykonana zostaa przez autora z zastosowaniem nast pujcych zasad: x podziau obiektu na funkcje rzeczywiste i nierzeczywiste, x wyodr bnienia rozcznych funkcji zalenociowych odpowiadajcych funkcjom realizowanym przez obiekt1, x wyodr bnienia funkcji powtarzalnych w innych obiektach, x tworzenia grafów z wykorzystaniem powtarzalnych podgrafów. Przy formalizacji opisu wykorzystano dotychczasowe publikacje z zakresu teorii grafów, analizy systemowej, modelowania, syntezy logicznej i projektowania bezpiecznych systemów sterowania zawarte w pracach [6, 14, 16, 21, 23,].. 1. Rozczno

(22) funkcji zalenociowych jest tu rozumiana, jako rozczno

(23) pomi dzy realizowanymi funkcjami sterowania. Dla obiektu iloczyn logiczny kadej pary dwóch funkcji zalenociowych jest zbiorem pustym..

(24) 40. Dariusz Koliski. 3. FORMALIZACJA OPISU Do odwzorowania systemu zalenociowego dowolnego posterunku ruchu w postaci schematu powiza ukadu torowego i obiektów uywane s powtarzalne obiekty odwzorowujce elementy systemu zalenociowego (rys. 2.2.). Poniewa ilo

(25) obiektów srk jest skoczona, zatem Postulat 1 Ka dy system zale no ciowy da si

(26) odwzorowa stosujc obiekty z poni szego zbioru obiektów:. Osrk = {J, L, T, Z, W, K, S, M, B, P}. (3.1). gdzie: Osrk – zbiór obiektów systemu srk, J – obiekt odwzorowujcy odcinek torowy krótki (bez prawa postoju taboru), L – obiekt odwzorowujcy odcinek torowy dugi (z prawem postoju taboru), T – obiekt odwzorowujcy skrzyowanie torów, Z – obiekt odwzorowujcy rozjazd zwyczajny, W – obiekt odwzorowujcy wykolejnic , K – obiekt odwzorowujcy rozjazd krzyowy, S – obiekt odwzorowujcy semafor, M – obiekt odwzorowujcy tarcz manewrow, B – obiekt odwzorowujcy blokad liniow, P – obiekt odwzorowujcy przejazd. Zdefiniowanie zbioru obiektów umoliwia przejcie do definiowania funkcji zalenociowych w obiektach (funkcji sterowa).. Dekompozycja obiektów na funkcje Zgodnie z przyj tym powyej zaoeniem funkcja sterowa obiektu jest sum funkcji sterowa rzeczywistych i nierzeczywistych, co moemy zapisa

(27). f ob = * f rzecz * f nierzecz. (3.2). gdzie: fob – funkcja sterowa obiektu, frzecz – funkcja sterowa rzeczywistych, fnierzecz – funkcja sterowa nierzeczywistych. Pod poj ciem funkcji sterowa rzeczywistych naley rozumie

(28) te funkcje, które zwizane s z obserwowaln zmian stanu obiektu w warstwie wykonawczej. Natomiast funkcje nierzeczywiste to takie, które nie powoduj zmian stanu obiektu w warstwie wykonawczej. W artykule rozpatrywane s ukady sterowania ruchem kolejowym wykorzystujce ukady cyfrowe, zatem do ich opisu mona zastosowa

(29) metody stosowane do opisu ukadów logicznych i cyfrowych [22]. Ogólnym modelem matematycznym jest opis za pomoc automatu skoczonego z pami ci, co pozwala na przyj cie nast pujcego postulatu.

(30) Formalny opis funkcji zalenociowych systemów srk dla wspóczesnych …. 41. Postulat 2 Ka d zdekomponowan funkcj

(31) sterowa rzeczywistych lub nierzeczywistych da si

(32) odwzorowa w postaci grafu automatu sko czonego. Zatem, system zalenociowy AT mona opisa

(33) jako m. n. AT = ** Ai. j. j 1 i 1. (3.3). gdzie: AT – system zalenociowy sterowania ruchem kolejowym (zbiór automatów systemu srk), Aji – i-ty automat j-tej funkcji sterujcej (rzeczywistej lub nierzeczywistej). Zgodnie z definicj skoczonego automatu Moore’a z pami ci opisujemy go jako pitk uporzdkowan [22]. A j = ( X j , Sj , Y j ,G j , Oj ). (3.4). gdzie: Xj = {xjn, …, xj1} – zbiór liter wejciowych (alfabet wejciowy) skoczony i niepusty dla j-tego automatu, Sj = {sjk, …, sj1} – zbiór stanów wewn trznych (alfabet wewn trzny) skoczony i niepusty dla j-tego automatu, Yj = {yjm, …, yj1} – zbiór liter wyjciowych (alfabet wyjciowy) skoczony i niepusty dla j-tego automatu, j: Dj Sj – funkcja przej

(34) dla j-tego automatu, j : Dj Yj – funkcja wyj

(35) dla j-tego automatu, Dj Xj u Sj, Dj Sj. Zbiór liter wejciowych skada si z trzech zbiorów: x zbiór liter wejciowych wewn trznych pochodzcych z wyj

(36) innych funkcji tego samego obiektu, x zbiór liter wejciowych zewn trznych pochodzcych z warstwy nadrz dnej, x zbiór liter wejciowych zewn trznych pochodzcych z warstwy wykonawczej. Zbiór liter wejciowych mona przedstawi

(37) w postaci sumy trzech rozcznych zbiorów. Xj j X wj X zwn. j j X wj X zwn X zww. j j j I X wj X zww I X zwn X zww I. (3.5) (3.6). gdzie: X jw – zbiór liter wejciowych wewn trznych pochodzcych z wyj

(38) innych funkcji tego samego obiektu, X jzwn – zbiór liter wejciowych zewn trznych pochodzcych z warstwy nadrz dnej, X jzww – zbiór liter wejciowych zewn trznych pochodzcych z warstwy wykonawczej..

(39) 42. Dariusz Koliski. Opis formalny na poziomie grafu automatu Dotychczasowe próby opisu systemu zalenociowego koncentroway si na opisie zewn trznym, który definiuje odpowiedzi na wyjciach w zalenoci od stanu zmiennych wejciowych. Dla mikroprocesorowych systemów zalenociowych przygotowywano behawioralny opis funkcjonalny definiujcy oczekiwane odpowiedzi na wyjciach w zalenoci od stanu wej

(40) [1]. W opisie tym nie zdefiniowany jest proces przetwarzania zbioru liter wejciowych pozwalajcy ledzi

(41) zmiany zachodzce w systemie zalenociowym od momentu rozpocz cia cyklu przetwarzania programów sterujcych [2] do uzyskania zbioru liter wyjciowych. Ze wzgl du na brak peni wiedzy o procesie przetwarzania programów sterujcych w mikroprocesorowym systemie zalenociowym powinien by

(42) on traktowany jako „czarna skrzynka”. Programy te tworzone s w postaci moduów programowych [1]. Dla poszczególnych moduów przeprowadza si analizy prawdopodobiestwa poprawnego wykonania moduu programu i przedstawia je w postaci macierzy prawdopodobiestw przej

(43) pomi dzy moduami [17]. Dla zapewnienia bezpieczestwa realizacji zalenoci stosuje si róne zabiegi na poziomie programowym i sprz towym oraz przeprowadza si testowanie funkcjonalne zbudowanego systemu zalenociowego. Takie podejcie polegajce na podawaniu sygnaów na wejciach i obserwowaniu uzyskanych odpowiedzi na wyjciach, jest równie stosowane przy sprawdzeniach i testach wyprodukowanych systemów zalenociowych. Podczas takich testów po podaniu zmiennych wejciowych bada si czy na wyjciu pojawiy si odpowiedzi nalece do zbioru odpowiedzi dopuszczalnych. Konsekwencj takiego podejcia jest potrzeba opracowywania macierzy opisujcych prawdopodobiestwo poprawnego wykonania programu (lub moduu programu) [17], aby oceni

(44) zachowanie systemu. Akceptacja takiej metody testowania wiadczy, e „historia” wygenerowania odpowiedzi na wyjciu systemu zalenociowego, jest nie znana od „wewntrz”. Zast pczo stosowany jest opis systemu zalenociowego równowaony pewnymi relacjami pomi dzy wektorem wejciowym a wektorem wyjciowym. Rozwizaniem problemu ledzenia zmian zachodzcych w procesie sterowania wykonywanym w systemie zalenociowym, jest odwzorowanie funkcji zalenociowych w postaci automatów, co eliminuje powysze ograniczenia a system zalenociowy staje si systemem „kontrolowalnym i przewidywalnym od wewntrz”. Wynika to z faktu, e oprócz zbiorów wejciowego i wyjciowego, wprowadzony zostaje take zbiór stanów wewn trznych pozwalajcy na ledzenie „historii” zmian, jak równie okrelenie odpowiedzi na podstawie zbioru wejciowego i wiedzy o aktualnym stanie wewn trznym. Poniewa w dalszej cz ci pracy b dzie mowa tylko o automatach Moore’a, zatem zbiór stanów wewn trznych automatu jest tosamy ze zbiorem wierzchoków grafu a wektor wyjciowy zaley tylko od stanu, w którym znajduje si automat, co zapisujemy. Yr j = Oj (Srj ) gdzie: Y jr – jest wektorem wyjciowym dla j-tego automatu w stanie r, j – jest funkcj wyj

(45) dla j-tego automatu, S jr – jest stanem wewn trznym r j-tego automatu.. (3.7).

(46) Formalny opis funkcji zalenociowych systemów srk dla wspóczesnych …. 43. Przejcie ze stanu Sk (wierzchoka Sk) do stanu Sr (wierzchoka Sr) pod wpywem pobudzenia pkr odpowiada zorientowanej kraw dzi grafu (ukowi, tranzycji) czcej stan Sk ze stanem Sr, opisanej pobudzeniem ppr, co mona zapisa

(47) w postaci. Srj = G j ( X kj , pkrj ). (3.8). gdzie: pjkr – jest pobudzeniem dla przejcia ze stanu Sk do Sr dla j-tego automatu. Natomiast macierz pobudze dla grafu automatu b dzie iloczynem Hadamarda (iloczynem po wspórz dnych), opisanym Pj = T j Wj. (3.9). gdzie: Pj – jest macierz pobudze dla j-tego automatu, Tj – jest macierz istnienia tranzycji dla j-tego automatu, w której 1 oznacza istnienie tranzycji a, 0 oznacza nie istnienie tranzycji, Wj – jest macierz warunków opisujcych tranzycje dla j-tego automatu, Natomiast pojedyncze pobudzenie jest opisane jako. pkrj = tkrj wkrj. (3.10). gdzie: pjkr – jest pobudzeniem dla przejcia ze stanu Sk do Sr dla j-tego automatu, tjkr – jest opisem istnienia tranzycji ze stanu Sk do Sr dla j-tego automatu, wjkr – jest warunkiem przejcia ze stanu Sk do Sr dla j-tego automatu. Zatem funkcja przej

(48) przyjmuje posta

(49). ª (t11j w11j ) « j (t w j ) ' j = « 21 21 « # « j j (t ¬« n1 wn1 ). (t12j w12j ) j (t 22 w22j ) # j (t n2 wnj2 ). " " % ". (t1nj w1jn ) º » j (t 2n w2jn ) » » # j » j (t nn wnn ) ¼». (3.11). Powysza macierz b dzie zawsze macierz kwadratow n x n o nast pujcych cechach: x wektor zbudowany z elementów dowolnego wiersza p opisuje warunki przejcia ze stanu p (wierzchoka p) do wszystkich stanów automatu (wierzchoków grafu), x wektor zbudowany z elementów dowolnej kolumny q opisuje warunki przejcia ze wszystkich stanów automatu do stanu q, x wektor zbudowany z elementów lecy na przektnej 11 do nn opisuje warunki pozostawania w poszczególnych stanach automatu. W systemie zalenociowym wanym zagadnieniem jest uwzgl dnienie wszystkich warunków okrelajcych przejcia ze stanu Sk do wszystkich stanów automatu jak równie kolejno

(50) przej

(51) do tych stanów. Std koniecznie jest okrelenie warunku pozostawania.

(52) 44. Dariusz Koliski. w tym samym stanie oraz opracowanie macierzy priorytetów przej

(53) . Warunek pozostawania w tym samym stanie jest negacj sumy warunków przej

(54) do stanów poprzedzajcych stan rozpatrywany oraz warunków nast pnych po rozpatrywanym stanie, co zapisujemy nast pujcy sposób k -1. w kr = * w kr . k r. r 1. n. *w. kr. r k 1. (3.12). Jeeli istnieje tranzycja pomi dzy dwoma dowolnymi stanami automatu k i r, to istnieje tylko jeden warunek opisujcy przejcie pomi dzy tymi stanami.. t krj 1 !wkr W. (3.13). Ostatnim istotnym elementem dla opisu funkcji zalenociowej w postaci automatu jest ustalenie kolejnoci rozpatrywania warunków przej

(55) (wjkx) przypisanych tranzycjom, wychodzcym ze stanu k. Kadej tranzycji przypisywana jest liczba (nazywana priorytetem) oznaczajca kolejno

(56) rozpatrywania przypisanego jej warunku. Im nisza jest liczba, tym wyszy jest priorytet warunku. Macierzy priorytetów dla automatu nie da si utworzy

(57) bezporednio z opisu behawioralnego, albowiem twórcy zapisów prawnych i literaturowych pomijaj to zagadnienie. Najlepsz moliw regu do stosowania jest zasada projektowania urzdze srk mówica, e urzdzenie srk powinno w pierwszym moliwym cyklu sterowania przej

(58) do stanu bezpiecznego. Przykadowa macierz priorytetów dla grafu z szecioma stanami moe mie

(59) posta

(60). P 6u6. ª6 «1 « «1 =« «3 «1 « ¬«5. 1 2 5 3 4º 6 3 4 2 5»» 3 6 4 2 5» » 1 5 6 4 2» 2 4 3 6 1» » 4 1 2 3 6¼». (3.14). Cechami charakterystycznymi macierzy priorytetów przej

(61) s nast pujce reguy: x kolejno

(62) sprawdzania warunków przej

(63) jest uszeregowana od najmniejszej do najwi kszej liczby, x liczby w kadym wierszu porzdkuj kolejno

(64) sprawdzana warunków przejcia ze stanu odpowiadajcego numerowi wiersza do pozostaych stanów automatu, x liczby w wierszu nie mog si powtarza

(65) , x na przektnej wyst puje najwi ksza liczba. Ustalenie priorytetów ma istotne znaczenie przy implementacji funkcji zalenociowych, albowiem przy naturalnym przejciu do sieci dziaa algorytmu lub graficznego schematu algorytmu (GSA) wane jest ustalenie kolejnoci rozmieszczenia klatek zawierajcych warunki i operacje..

(66) Formalny opis funkcji zalenociowych systemów srk dla wspóczesnych …. 45. Opis formalny pocze na poziomach hierarchicznych. Z uwagi na przyj ty powyej sposób opisu obiektów srk O oraz systemu zalenociowego AT, konieczne jest zdefiniowanie pocze wewn trznych pomi dzy: x funkcjami zalenociowymi na poziomie obiektu, x obiektami na poziomie systemu zalenociowego. Dla kadego obiektu przesyanie sygnaów wyjciowych z funkcji zalenociowych na ich wejcia mona przedstawi

(67) za pomoc macierzy opisanej w przestrzeni trójwymiarowej. B p u qu q. ª b111 b112 " b11q º » 2 « 1 21 2 b 21 ª bb11 b12q » b1q º " 22 b" 12 « = 2 2 » » « # « b 2# b% # " b 2q » 22 » q « 1 « 211 qb1 « b b " # # ª b% »b12# » ¬« p1 « p2 11 pq ¼ 2 2 « q 2 » bbq22pq ¼» 21 ¬« b p1 b p2 « b" « # # « q q «¬ b p1 b p2. " " % ". q º b1q q » b 2q » # » » b qpq »¼. (3.15). gdzie: B – jest przestrzeni liczb cakowitych nieujemnych, w której 0 oznacza brak poczenia a liczba b oznacza numer wejcia sygnau wewn trznego i naley do zbioru {0, 1, …, q}, bjxy – jest numerem wejcia y-owej funkcji zalenociowej, poczonej z x-owym wyjciem j-otej funkcji zalenociowej, p – jest maksymaln liczb wyj

(68) funkcji zalenociowych w obiekcie, q – jest liczb funkcji zalenociowych w obiekcie. Stosowanie trójwymiarowej macierzy generuje automatycznie pojawianie si duej iloci zer w macierzy i w praktyce rozmazuje obraz pocze. Znacznie przyja niejsz form opisu jest utworzenie dla kadej funkcji zalenociowej indywidualnej macierzy o postaci. Bj cuq. ª b11j « j b = « 21 « # « j ¬« b c1. b12j j b 22 # b c2j. " " % ". b1qj º j » b 2q » # » » b cqj ¼». (3.16). gdzie: c – jest liczb wyj

(69) j-otej funkcji zalenociowej w obiekcie (c p). Przy takim podejciu naley utworzy

(70) q macierzy dwuwymiarowych o wymiarach odpowiadajcych kadej funkcji. W analogiczny sposób mona opisa

(71) przesyanie sygnaów mi dzy obiektami O wewntrz systemu zalenociowego AT..

(72) 46. Dariusz Koliski. 4. ALGORYTMY TWORZENIA OPISU FORMALNEGO Przygotowanie opisu formalnego systemu zalenociowego wymaga zastosowania trzech rodzajów algorytmów: x algorytmu tworzenia formalnego opisu funkcji zalenociowej, x algorytmu tworzenia formalnego opisu obiektu, x algorytmu tworzenia formalnego opisu systemu zalenociowego. Algorytm tworzenia formalnego opisu funkcji zale no ciowej. Okrelenie zmiennych wejciowych (zbiór liter wejciowych Xj = {xjn, …, xj1}). Zbiór ten jest sum trzech rozcznych zbiorów: x zbioru zmiennych wejciowych wewn trznych pochodzcych z innych funkcji tego samego obiektu Xjw = {xjb, …, xj1}, x zbioru zmiennych wejciowych zewn trznych pochodzcych z warstwy nadrz dnej Xjzwn = {xjc, …, xjb+1}, x zbioru zmiennych wejciowych zewn trznych pochodzcych z warstwy wykonawczej, zawierajce równie zmienne o geometrii posterunku Xjzww = {xjn, …, xjc+1}, Okrelenie i nazwanie stanów automatu (wierzchoków grafu, zbioru stanów wewn trznych) Sj = {sjk, …, sj1}. Przypisanie poszczególnym stanom automatu (wierzchokom grafu) wartoci na wyjciach (zbiór liter wyjciowych) Yj = {yjm, …, yj1}. Okrelenie istnienia uków (przej

(73) ) pomi dzy stanami automatu (wierzchokami grafu) w postaci macierzy istnienia tranzycji Tj. Macierz ta jest macierz o wymiarach k x k. Przypisanie poszczególnym ukom (tranzycjom) warunków przej

(74) i utworzenie macierzy Wj. Macierz ta jest macierz o wymiarach k x k. Wyznaczenie funkcji przej

(75) (zaleno

(76) 3.11). Sprawdzenie poprawnoci warunku pozostawania w tym samym stanie (zaleno

(77) 3.12), Opracowanie macierzy priorytetów dla tranzycji. Macierz ta jest macierz o wymiarach k x k. Algorytm tworzenia formalnego opisu obiektu Podzia obiektu na rozczne funkcje zalenociowe, Okrelenie zmiennych wejciowych obiektu (zbiór liter wejciowych obiektu Xo = {xon, …, xo1}). Zbiór ten jest sum trzech rozcznych zbiorów: x zbioru zmiennych wejciowych wewn trznych pochodzcych z funkcji zalenociowych Xow = {xod, …, xo1}, x zbioru zmiennych wejciowe zewn trznych pochodzcych z warstwy nadrz dnej Xozwn = {xoe, …, xod+1}, x zbioru zmiennych wejciowych zewn trznych pochodzcych z warstwy wykonawczej, zawierajcej równie zmienne geometrii posterunku Xozww = {xon, …, xoe+1},.

(78) Formalny opis funkcji zalenociowych systemów srk dla wspóczesnych …. 47. Kady z trzech powyszych zbiorów jest sum logiczn odpowiadajcych im zbiorów liter wejciowych funkcji zalenociowych obiektu, Opracowanie dla kadej z funkcji zalenociowych macierzy pocze wewn trznych, Okrelenie zmiennych wyjciowych obiektu (zbiór liter wyjciowych obiektu) Yo = {yon, …, yo1}. Zbiór liter wyjciowych obiektu jest logiczn sum zbiorów liter wyjciowych funkcji obiektu. Algorytm tworzenia formalnego opisu systemu zale no ciowego Okrelenie zbioru obiektów odzwierciedlajcych system zalenociowy posterunku ruchu, Okrelenie zmiennych wejciowych obiektu (zbiór liter wejciowych obiektu) XAT = {xATn, …, xAT1}. Zbiór ten jest sum trzech rozcznych zbiorów: x zbioru zmiennych wejciowych wewn trznych pochodzcych z innych obiektów XATw = {xATg, …, xAT1}, x zbioru zmiennych wejciowych zewn trznych pochodzcych z warstwy nadrz dnej XATzwn = {xATh, …, xATg+1}, x zbioru zmiennych wejciowych zewn trznych pochodzcych z warstwy wykonawczej, zawierajcej równie zmienne geometrii posterunku XATzww = {xATn, …, xATh+1}, Kady z trzech powyszych zbiorów jest sum logiczn odpowiadajcych im zbiorów liter wejciowych funkcji obiektu, Opracowanie macierzy pocze wewn trznych dla kadego obiektu, Okrelenie zmiennych wyjciowych obiektu (zbiór liter wyjciowych obiektu) YAT = {yATn, …, yAT1}. Zbiór ten jest logiczn sum zbiorów liter wyjciowych obiektów. Stosujc dekompozycj obiektów na funkcje dokonano opisu formalnego wyodr bnionych funkcji zalenociowych. Opracowane funkcje zalenociowe zestawiono w tablicy 4.1. W poniszym zestawieniu uwzgl dniono rozrónienie funkcji rzeczywistych i nierzeczywistych. cznie w obiektach wyodr bniono 57 funkcji, przy czym 18 z nich jest powtarzalnych, zatem wystarczajcy zbiór funkcji do opracowania 10 obiektów liczy 39 funkcji zalenociowych. W zapisie symbolicznym funkcji litera to symbol obiektu a indeks górny oznacza numer funkcji obiekcie..

(79) 48. Dariusz Koliski. Tablica 4.1. Funkcje zale no ciowe po dekompozycji obiektów Funkcja Nr. Rzeczywista Nierzeczywista Nazwa Symbol Nazwa Symbol 1 Odcinek torowy krótki (bez prawa postoju) J kontroli niezaj toci odcinka torowego J1 utwierdzenia odcinka torowego J2 zamkni cia odcinka torowego J3 2 Odcinek torowy dugi (z prawem postoju) L L2 kontroli niezaj toci odcinka torowego L1=J1 utwierdzenia odcinka torowego zamkni cia odcinka torowego L3=J3 3 Skrzy owanie torów T kontroli niezaj toci skrzyowania torów T1=J1 utwierdzenia skrzyowania torów T2 zamkni cia skrzyowania torów T3=J3 4 Rozjazd zwyczajny Z Z3 kontroli niezaj toci odcinka zwrotnicowego Z1=J1 utwierdzenia rozjazdu kontroli pooenia zwrotnicy Z2 utwierdzenia rozjazdu w drodze ochronnej Z4 utwierdzenia rozjazdu w ochronie bocznej Z5 stopowania pooenia zwrotnicy Z6 zamkni cia rozjazdu Z7=J3 lokalnego przestawiania zwrotnicy Z8 5 Wykolejnica W W3 kontroli niezaj toci odcinka torowego W1=J1 utwierdzenia wykolejnicy 2 kontroli pooenia wykolejnicy W utwierdzenia wykolejnicy w drodze ochronnej W4 utwierdzenia wykolejnicy w ochronie bocznej W5 stopowania wykolejnicy W6=Z6 zamkni cia wykolejnicy W7=J3 lokalnego przestawiania wykolejnicy Z8 6 Rozjazd krzy owy K kontroli niezaj toci odcinka zwrotnicowego K1=J1 utwierdzenia rozjazdu K4 kontroli pooenia zwrotnicy ab K2 utwierdzenia rozjazdu w drodze ochronnej K5 kontroli pooenia zwrotnicy cd K3=K2 utwierdzenia zwrotnicy ab w ochronie bocznej K6 utwierdzenia zwrotnicy cd w ochronie bocznej K7=K6 stopowania zwrotnicy ab K8=Z6 stopowania zwrotnicy cd K9=Z6 zamkni cia rozjazdu K10=J3 lokalnego przestawiania zwrotnicy ab K11 lokalnego przestawiania zwrotnicy cd K12=K11 7 Semafor S stopowania semafora S7 kontroli wiata górnego S1 kontroli wiata dolnego S2 przebiegu pocigowego S8 kontroli wska ników W19 i W20 S3 przebiegu manewrowego S9 kontroli wska ników W24 i W26 S4 wywietlanie sygnaów S5 sygnau zast pczego S6 8 Tarcza manewrowa M kontroli wiate tarczy manewrowej M1 stopowania tarczy manewrowej M3=S7 wywietlania sygnaów tarczy manewrowej M2 przebiegu manewrowego M4=S9 9 Blokada liniowa B kontroli niezaj toci pierwszego odst pu B1=J1 stopowania wyjazdu na szlak B3 blokady 2 kontroli kierunku B kontroli wiata górnego nast pnego semafora B4=S1 5 kontroli wiata dolnego nast pnego semafora B =S2 10 Przejazd P kontroli pooenia przejazdu P1 utwierdzenia przejazdu P2.

(80) Formalny opis funkcji zalenociowych systemów srk dla wspóczesnych …. 49. Przykad tworzenia formalnego opisu funkcji zale no ciowej. Stosujc przedstawiony powyej algorytm tworzenia opisu funkcji zalenociowej, opisana zostanie funkcja kontroli niezaj toci (J1). Opis ten zaczyna si od okrelenia zbioru zmiennych wejciowych (zbiór liter wejciowych), który ma posta

(81) : x 1J1. x J21. X J1 = {JT, uszkodzenie }. (4.1). gdzie: JT – informacja o stanie zaj toci lub niezaj toci odcinka torowego przesyana z warstwy wykonawczej. Uszkodzenie – informacja o stanie sprawnoci ukadu kontroli izolacji torowej przesyana z warstwy wykonawczej. Podzia tego zbioru na trzy podzbiory jest nast pujcy: x zmienne wejciowe wewn trzne pochodzce z innych funkcji tego samego obiektu X Jw1 = I. (4.2). x zmienne wejciowe zewn trzne pochodzce z warstwy nadrz dnej 1 X Jzwn =I. (4.3). x zmienne wejciowe zewn trzne pochodzce z warstwy wykonawczej, zawierajce równie zmienne geometrii posterunku 1 X Jzww = X J1. (4.4). Zbiór stanów wewn trznych (wierzchoków grafu) jest nast pujcy 101. 102. 103. J1. S = {wolny, zajety, uszkodzony}. (4.5). Nast pnie poszczególnym stanom automatu (wierzchokom grafu) przypisano wartoci na wyjciach (zbiór liter wyjciowych) J1 Y101 = {1} J1 Y102 = {0} J1 Y103 = {0}. Z tych zbiorów wartoci mona zbudowa

(82) macierz wartoci o postaci:. (4.6) (4.7) (4.8).

(83) 50. Dariusz Koliski. JT_stan 101 W ª 1 º « 0 » » « «¬ 0 »¼. Y J1 = 102 Z 103 U. (4.9). gdzie: 101-103 – numery wierzchoków, W, Z, U – nazwy stanów (odpowiednio Wolny, Zaj ty, Uszkodzony). Kolejnym krokiem jest okrelenie istnienia uków (przej

(84) ) pomi dzy stanami automatu (wierzchokami grafu) w postaci macierzy istnienia tranzycji TJ1. Macierz ta jest macierz o wymiarach 3 x 3. 101 101 W T J1 102 Z 103 U. W ª1 «1 « «¬0. 102. 103. Z 1. U 1º 1»» 1»¼. 1 1. (4.10). Odpowiednio przypisano poszczególnym ukom (tranzycjom) warunki przej

(85) za pomoc macierzy nast pujcej postaci 101. 102. 103. W. Z. U. ªJT Uszkodzenie JT Uszkodzenieº « » 102 Z «JT Uszkodzenie JT Uszkodzenie Uszkodzenie» 103 U «¬ 1 Uszkodzenie Uszkodzenie»¼ 101 W. W. J1. (4.11). gdzie: 1 – oznacza dowolny warunek. Zatem, funkcja przej

(86) b dzie mie

(87) posta

(88) 101. 102. 103. W. Z. U. ªJT Uszkodzenie JT Uszkodzenieº « » 102 Z «JT Uszkodzenie JT Uszkodzenie Uszkodzenie» 103 U «¬ 0 Uszkodzenie Uszkodzenie»¼ 101 W. '. J1. Ostatni czynnoci jest opracowanie macierzy priorytetów, która ma posta

(89). (4.12).

(90) Formalny opis funkcji zalenociowych systemów srk dla wspóczesnych …. P. J1. ª3 1 2 º «1 3 2 » » « «¬0 1 2»¼. 51. (4.13). gdzie: 0 – oznacza, e nie mona przypisa

(91) priorytetu, poniewa nie istnieje uk.. 5. PODSUMOWANIE Przedstawiona metoda opisu formalnego funkcji zalenociowych pozwala na ich opis, bez stosowania „rozmytych” zwrotów lingwistycznych jak np. „mog by

(92) ”, „musz spenia

(93) ”, „dopuszcza si ”, „naley realizowa

(94) ”, „powinno spenia

(95) ”. Zwroty takie s stosowane mi dzy innymi w wytycznych technicznych budowy urzdze srk [20]. Zastosowana metoda pozwolia na przygotowanie opisów formalnych 39 funkcji zalenociowych, które posuyy do utworzenia obiektów srk. Poprawno

(96) opracowanych funkcji zalenociowych, jak równie obiektów mona potwierdzi

(97) analizujc poszczególne macierze, jednake jest to bardzo czasochonne i nieefektywne. Do procesu weryfikacji zastosowano wspomaganie komputerowe w postaci pakietu Active-HDL. Pakiet ten pozwoli na podstawie opracowanych wzorów i macierzy wyspecyfikowa

(98) grafy automatów funkcji zalenociowych w edytorze FSM, a nast pnie po wygenerowaniu opisu w j zyku VHDL, umoliwi przeprowadzenie symulacji w trybie funkcjonalnym. Analogiczny proces specyfikacji i weryfikacji przeprowadzony zosta na poziomie obiektów z wykorzystaniem edytora hierarchicznych schematów blokowych BDE. W przeprowadzonym procesie testowania mona ledzi

(99) „histori ” zmian zachodzcych na dowolnym poziomie zoonoci(funkcja, obiekt, system zalenociowy). Uzyskane opisy macierzowe funkcji zalenociowych pozwalaj przej

(100) do algorytmu sterowania [7] lub graficznego schematu algorytmu (GSA) [5, 14], co pozwala na praktyczne projektowanie systemów zalenociowych niezalenie od techniki.. Bibliografia 1. PKP – Centrum Naukowo Techniczne Kolejnictwa: Wymagania bezpiecze stwa dla urzdze sterowania ruchem kolejowym. CNTK, Warszawa, luty 1998. 2. Dbrowa-Bajon M.: Podstawy sterowania ruchem kolejowym. Funkcje, wspomagania, zarys techniki. Wydanie 2 poprawione. Oficyna Wydawnicza Politechniki Warszawskiej, Warszawa, 2007 r. 3. Dbrowa-Bajon M., Karbowiak H., Grochowski K.: Zasady projektowania systemów i urzdze sterowania ruchem kolejowym. WK, Warszawa, 1981 r. 4. Centralne Biuro Projektowo-Badawcze Budownictwa Kolejowego: Album schematów przeka nikowych urzdze zabezpieczenia ruchu kolejowego typu E. Aktualizacja 1989. Warszawa, 1989 r. 5. Firlg K.: Metoda projektowania urzdze sterowania ruchem drogowym w reprogramowalnych strukturach logicznych, Oficyna Wydawnicza Politechniki Warszawskiej, Warszawa, 2010r. 6. Kacprzyk J.: Zbiory rozmyte w analizie systemowej. PWN, Warszawa, 1986 r..

(101) 52. Dariusz Koliski. 7. Kawalec P., Koliski D.: Algorytmizacja funkcji sterujcych samoczynnych sygnalizacji przejazdowych. Materiay VII Konferencji „Komputerowe systemy wspomagania nauki, przemysu i transportu TRANSCOMP”, Zakopane, 2003, str. 255-260. 8. Kawalec P., Koliski D.: Specyfikacja i weryfikacja elektronicznych komparatorów funkcji sterujcych urzdze srk. Politechnika Radomska, Prace Naukowe – Elektryka nr 2 (8) 2004, Radom, 2004, str. 87 – 92. 9. Kawalec P., Koliski D.: Zastosowanie j zyków opisu sprz tu do modelowania elementów srk o charakterystyce przeka nikowej. Politechnika Radomska, Prace Naukowe – Elektryka nr 1 (9) 2005, Radom, 2005, str. 107 – 112. 10. Kawalec P., Koliski D.: Modelowanie obwodów przeka nikowych urzdze srk w j zykach opisu sprz tu. Politechnika Radomska, Prace Naukowe – Elektryka nr 1 (9) 2005, Radom, 2005, str. 101 – 106. 11. Kawalec P., Koliski D.: Analiza i synteza trójkanaowej samoczynnej sygnalizacji przejazdowej w strukturach FPGA. Politechnika Warszawska, Prace Naukowe –Transport, z 56, OWPW, Warszawa, 2006, str. 61 – 85. 12. Kawalec P., Koliski D.: Modelowanie Interlocking’u z zastosowaniem j zyka opisu sprz tu. Logistyka 6/2010, Pozna, 2010, str. 1329 – 1337. 13. Kawalec P., Koliski D.: Jednoznaczna metoda opisu funkcji zalenociowych w systemach sterowania ruchem kolejowym. Logistyka 6/2011, Pozna, 2011, str. 1585 – 1594. 14. Kawalec P.: Analiza i synteza specjalizowanych ukadów modelowania i sterowania ruchem w transporcie. Politechnika Warszawska, Prace Naukowe – Transport, z. 68, Oficyna Wydawnicza Politechniki Warszawskiej, Warszawa, 2009 r. 15. Kawalec P., Koliski D., Mocki J.: Zastosowanie programowalnych struktur logicznych w projektowaniu urzdze sterowania ruchem kolejowym. Problemy kolejnictwa, Nr 140, CNTK, Warszawa, 2005, str. 66 – 88. 16. Korzan B.: Elementy teorii grafów i sieci. Metody i zastosowania. WNT, Warszawa, 1978 r. 17. Lewiski A.: Problemy oprogramowania bezpiecznych systemów komputerowych w zastosowaniach transportu kolejowego. Politechnika Radomska, Monografie Nr 49, Radom, 2001 r. 18. uba T., Nowicka M., Perkowska M., Rawski M.: Nowoczesna synteza logiczna. Oficyna Wydawnicza Politechniki Warszawskiej, Warszawa, 1998 r. 19. Mikulczyski T., Samsonowicz Z.: Automatyzacje dyskretnych procesów produkcyjnych. Metody modelowania procesów dyskretnych i programowania PLC. WNT, Warszawa, 1997 r. 20. PKP Dyrekcja Generalna: Wytyczne techniczne budowy urzdze sterowania ruchem kolejowym w przedsi biorstwie Polskie Koleje Pastwowe (WTB-E10). Warszawa, 1996 r. 21. Saponikow V. V., Hristov H. A., Gawzow D. W.: Mietody postrojenia biezopastnych mikroeliektronnych sistiem elieznodoronoj avtomatiki. Transport. Moskwa, 1995 r. 22. Traczyk W.: Ukady cyfrowe – podstawy teoretyczne i metody syntezy. WNT, Warszawa, 1982 r. 23. Zabocki W.: Modelowanie stacyjnych systemów sterowania ruchem kolejowym. Politechnika Warszawska, Prace Naukowe – Transport, z. 65, Oficyna Wydawnicza Politechniki Warszawskiej, Warszawa, 2008 r.. FORMAL DESCRIPTION OF INTERLOCKING FUNCTIONS OF RAILWAY TRAFFIC CONTROL SYSTEMS Summary: The article indicates the need for designing a formal description of interlocking functions. Based on the currently used representation of interlocking system in the form of objects, a formal description of interlocking functions has been proposed of objects created from designed functions and a description of interlocking system created of objects. The application of some elements of the theory of graphs, automata and sets allowed for designing a formal description in which interlocking system is no longer a “black box”. The designed description method allows for tracking the history of changes within interlocking system. The division of objects of interlocking system into interlocking functions has also been presented. Keywords: railway traffic control, dependence system, formal description.

(102)