!
Piotr Kawalec, Marcin R"ysko
Politechnika Warszawska, Wydzia7 TransportuMETODA
TWORZENIA
FORMALNEGO
ZAPISU
ALGORYTMÓW
DZIA'ANIA
URZ(DZE)
SRK
R9kopis dostarczono, marzec 2013
Streszczenie: W artykule przedstawiono problemy formalnego zapisu algorytmów dzia7ania urz?dze@
zabezpieczenia ruchu kolejowego oraz wspomaganej komputerowo specyfikacji tych algorytmów z wykorzystaniem j9zyków opisu sprz9tu. Przegl?d stosowanych obecnie metod opisu urz?dze@ srk wskazuje, De nie istnieje metoda, która mog7aby zapewniF jednolit? platform9 opisu wszelkiego rodzaju dyskretnych uk7adów sterowania. Wi9kszoGF stosowanych metod opisu nie pozwala na wykorzystanie wspomagania komputerowego na etapie specyfikacji i weryfikacji algorytmów dzia7ania tego typu uk7adów. Zosta7o pokazane, De zastosowanie do tego celu j9zyków opisu sprz9tu tworzy jednolit? platform9 specyfikacji i weryfikacji urz?dze@ srk, pozwalaj?c dodatkowo na statyczn? i dynamiczn? weryfikacj9 poprawnoGci opisu z wykorzystaniem wspomagania komputerowego w postaci symulatorów logicznych. Na przyk7adzie specyfikacji algorytmu dzia7ania jednoodst9powej blokady liniowej w j9zyku VHDL zaprezentowane zosta7y zarówno moDliwoGci pakietu Active-HDL, jak i proces wspomaganej komputerowo specyfikacji i weryfikacji projektowanego uk7adu.
S+owa kluczowe: j9zyk VHDL, blokada liniowa, sterowanie ruchem kolejowym
1. WST/P
Urz?dzenia sterowania ruchem kolejowym spe7niaF musz? rygorystyczne warunki w zakresie bezpiecze@stwa i niezawodnoGci dzia7ania. KaDdy b7?d w ich funkcjonowaniu moDe potencjalnie prowadziF do zagroDenia Dycia ludzkiego i wysokich strat materialnych. Yród7em b79dów, oprócz uszkodze@ sprz9towych, moDe byF niew7aGciwie wykonana specyfikacja. Dlatego wraz z rosn?c? niezawodnoGci? elementów, z których budowane s? urz?dzenia, zwi9kszaF musi si9 takDe pewnoGF metod projektowania.
W przypadku urz?dze@ zabezpieczenia ruchu poci?gów stosowanych jest wiele metod opisu zaleDnie od wybranej techniki realizacji. W ostatnich latach najcz9Gciej zabudowywane s? urz?dzenia komputerowe. Obecna tendencja do obejmowania coraz wi9kszych obszarów sterowaniem z jednej nastawni (tzw. Lokalne Centra Sterowania) powoduje, iD znacz?co wzrasta iloGF funkcji realizowanych przez poszczególne systemy srk.
KoniecznoGF wspó7pracy wielu typów urz?dze@ (systemy zaleDnoGciowe, blokady liniowe, systemy przekazywania informacji o poci?gu, uk7ady diagnostyki taboru) w obr9bie jednego obszaru sterowania powoduje, De niezb9dne staje si9 opracowanie jednolitej i spójnej platformy projektowej i opisowej dla róDnych rodzajów urz?dze@ i systemów sterowania ruchem kolejowym.
Artyku7 przedstawia koncepcj9 wykorzystania do stworzenia takiej platformy j9zyków opisu sprz9tu wraz z dedykowanymi narz9dziami wspomagania komputerowego. Udowodniona zosta7a przydatnoGF wykorzystania wspomagania komputerowego do szczegó7owej analizy dzia7ania urz?dze@ przeka_nikowych [7]. Poruszany jest równieD w pracach naukowych temat zastosowania w technice srk uk7adów programowalnych, tworzonych przy uDyciu j9zyków opisu sprz9tu [6]. Niniejszy artyku7 opisuje proces budowy algorytmu dzia7ania dla przyk7adowego urz?dzenia sterowania ruchem kolejowym oraz metody specyfikacji i weryfikacji tego algorytmu z wykorzystaniem wspomagania komputerowego.
2. METODY
OPISU
URZ(DZE)
SRK
Pierwotnie urz?dzenia sterowania ruchem kolejowym opiera7y si9 g7ównie na zaleDnoGciach mechanicznych. W celu pokazania i opisania zasady ich dzia7ania opracowywane by7y szczegó7owe opisy s7owne, wzbogacane rysunkami poszczególnych elementów i schematami ich wspó7pracy [10]. Projektowanie takich urz?dze@ by7o procesem d7ugotrwa7ym i skomplikowanym, gdyD aby upewniF si9, czy urz?dzenie zadzia7a poprawnie, konieczne by7o wybudowanie prototypu i jego przetestowanie. Sam opis stanowi7 jedynie zapis idei i wytyczne do konstrukcji.
W przypadku urz?dze@ elektrycznych czy przeka_nikowych najpowszechniejsz? form? opisu s? schematy elektryczne [14]. Schemat taki odzwierciedla fizyczne po7?czenie poszczególnych elementów uk7adu, jest wi9c dogodn? form? do montaDu. Jako metoda projektowania opiera si9 wy7?cznie na doGwiadczeniu projektanta. MoDliwa jest tylko statyczna analiza uk7adu, która jednak w przypadku z7oDonych uk7adów staje si9 Dmudna i d7ugotrwa7a, nie daj?c wci?D gwarancji, De urz?dzenie w ogóle uda si9 uruchomiF.
Graficzne metody opisu, takie jak schematy blokowe algorytmu stosowane s? cz9sto przy projektowaniu urz?dze@ komputerowych, stanowi? jednak tylko poGredni etap syntezy. Bez narz9dzi wspomagania komputerowego nie jest bowiem moDliwe automatyczne przekszta7cenie tak stworzonego modelu w program gotowy do zaimplementowania w urz?dzeniu. Takie narz9dzia s? juD, co prawda wykorzystywane do pojedynczych rozwi?za@, jednak ich zastosowanie ograniczone jest do konkretnego urz?dzenia, nie mog? wi9c stanowiF uniwersalnej platformy projektowej.
Opisane metody projektowania to w wi9kszoGci metody heurystyczne, niepozwalaj?ce na jednoznaczne stwierdzenie, De wykonany projekt uwzgl9dnia wszystkie moDliwe zachowania modelowanego uk7adu. Widoczny jest brak jednego, zunifikowanego Grodowiska, w którym proces projektowania by7by pozbawiony wymienionych niedogodnoGci. Prowadzone s? prace badawcze ukierunkowane na formalne metody specyfikacji urz?dze@ sterowania ruchem kolejowym [3, 5, 8, 9]. Proponowane by7y
specjalne j9zyki programowania dedykowane wy7?cznie projektowaniu takich uk7adów [2]. PodejGcie formalne minimalizuje ryzyko przeoczenia b79du w procesie tworzenia specyfikacji. NaleDy jednak zwróciF uwag9 na to, aby wybrana metoda by7a nieustannie wykorzystywana i rozwijana przez wiele branD automatyki, co zapewnia sta7y dost9p do najnowszych zdobyczy techniki w zakresie sprz9towym. Dlatego do stworzenia uniwersalnej platformy formalnego opisu urz?dze@ srk zaproponowane zosta7y j9zyki opisu sprz9tu.
3. J/ZYKI
OPISU
SPRZ/TU
Wykorzystanie j9zyków opisu sprz9tu (HDL – Hardware Description Languages) jest dziG popularnym podejGciem przy projektowaniu uk7adów elektronicznych, szczególnie w zastosowaniach wymagaj?cych wysokiej niezawodnoGci dzia7ania (lotnictwo, wojsko). J9zyki HDL umoDliwiaj? tworzenie sformalizowanego modelu dzia7ania uk7adu, b9d?cego zarówno zapisem projektu, jak i podstaw? do implementacji oraz wykonania prototypu. Od typowych j9zyków programowania odróDnia je to, De efektem prac, zamiast aplikacji uruchamianej w systemie operacyjnym komputera, moDe byF plik konfiguracyjny dla kompletnego uk7adu realizuj?cego zadane funkcje (na przyk7ad uk7adu FPGA).
W obecnym stanie rozwoju techniki cyfrowej i przy stale rosn?cej z7oDonoGci uk7adów trudno wyobraziF sobie projektowanie bez narz9dzi wspomagania komputerowego. PopularnoGF j9zyków opisu sprz9tu sprawia, De posiadaj? one wiele dedykowanych narz9dzi CAD (Computer Aided Design). Takie narz9dzia nie tylko upraszczaj? proces tworzenia kodu, ale takDe umoDliwiaj? automatyczn? weryfikacj9 oraz symulacj9 dzia7ania opracowanego modelu.
Dokonuj?c wyboru Grodowiska projektowania naleDy kierowaF si9 dost9pnoGci? takich narz9dzi CAD, które umoDliwiaj? prac9 nad projektem na kaDdym etapie (specyfikacja, weryfikacja, synteza, implementacja). Te warunki mog? zapewniF tylko j9zyki maj?ce status Gwiatowego standardu. Takim j9zykiem jest VHDL (VHSIC Hardware Decription
Language), j9zyk, który znalaz7 zastosowanie w modelowaniu z7oDonych uk7adów
cyfrowych w wielu branDach automatyki [4, 11]. Zosta7 stworzony w latach 80-tych na potrzeby Departamentu Obrony USA i jest stale rozwijany, ostatnia wersja zatwierdzona przez IEEE pochodzi z 2008 roku.
J9zyk VHDL wraz z dedykowanym pakietem wspomagania komputerowego zosta7 wykorzystany do opracowania metody specyfikacji, która stanowi zasadniczy cel tej pracy.
4. METODA PROJEKTOWANIA Z WYKORZYSTANIEM
WSPOMAGANIA KOMPUTEROWEGO
Zagadnienia formalnego zapisu algorytmu oraz korzyGci wynikaj?ce z zastosowania wspomagania komputerowego zaprezentowane zostan? na przyk7adowym projekcie algorytmu urz?dzenia srk. Poszczególne etapy prac to:
, stworzenie s7ownego opisu dzia7ania uk7adu, , budowa algorytmu na podstawie ogólnego opisu, , formalny zapis algorytmu,
, budowa grafu stanów automatu sko@czonego, , specyfikacja w j9zyku opisu sprz9tu.
Kolejne rozdzia7y opisuj? etapy specyfikacji i weryfikacji algorytmu dzia7ania modu7u logicznego jednoodst9powej blokady liniowej.
4.1. ZA'O4ENIA WST/PNE I OPIS S'OWNY
Projektowanie kaDdego urz?dzenia musi byF poprzedzone opisem wymaganych funkcji oraz sposobu ich realizacji. Najcz9Gciej stosowany jest opis s7owny, który moDe byF uzupe7niony o schematyczne rysunki wyjaGniaj?ce dzia7anie urz?dzenia.
Blokady liniowe to urz?dzenia, które zabezpieczaj? ruch poci?gów na szlaku, uzaleDniaj?c od siebie dzia7ania s?siednich posterunków ruchu. Podstawow? funkcj? tych uk7adów jest wi9c niedopuszczenie do pojawienia si9 na jednym torze szlakowym poci?gów jad?cych w przeciwnych kierunkach, oraz zachowanie odpowiedniego odst9pu pomi9dzy poci?gami poruszaj?cymi si9 w tym samym kierunku. Zgodnie z tradycyjnym podzia7em blokady liniowe dziel? si9 na pó7samoczynne i samoczynne [1]. Obecnie wdraDane rozwi?zania komputerowe to w zasadzie tylko blokady samoczynne. Uk7adowa kontrola niezaj9toGci szlaku pozwala na automatyczne stwierdzenie przyjazdu poci?gu w ca7oGci (nie jest wi9c konieczna kontrola wzrokowa, jak w przypadku klasycznych blokad pó7samoczynnych). DokonaF moDna jedynie podzia7u na blokady jednoodst9powe, gdzie ca7y szlak stanowi jeden odst9p, i wieloodst9powe, wykorzystuj?ce samoczynne semafory do podzia7u szlaku.
Opracowany algorytm blokady jednoodst9powej stworzony zosta7 w oparciu o instrukcj9 WTB-E10 [15] oraz zasad9 dzia7ania podobnych urz?dze@ tego typu, takich jak blokada typu Eac-95 [12]. Przyj9to nast9puj?ce za7oDenia dotycz?ce funkcjonalnoGci blokady:
, w stanie zasadniczym brak ustawionego kierunku,
, w7?czenie kierunku moDliwe tylko przy niezaj9toGci szlaku, , moDliwa awaryjna zmiana kierunku,
, samoczynne zwolnienie kierunku po wje_dzie poci?gu w przypadku linii jednotorowej,
, moDliwoGF zastopowania blokady.
Projektowana blokada sk7ada si9 z dwóch modu7ów (po jednym na obu przyleg7ych posterunkach ruchu) po7?czonych lini? transmisyjn?. Dzia7anie urz?dzenia opiera si9 na równoleg7ej realizacji powyDszych funkcji przez obydwa modu7y. Rys. 1 przedstawia schematyczne rozmieszczenie urz?dze@ blokady, kolorem szarym wyróDniono modu7y logiczne.
Rys. 1. Schemat ogólny urz?dze@ blokady liniowej
W stanie zasadniczym blokada nie ma ustawionego kierunku. JeGli dyDurny ruchu chce wyprawiF poci?g, musi uDyF do tego polecenia w7?czenia blokady, które powoduje wys7anie D?dania do s?siedniego posterunku (pod warunkiem, De szlak jest wolny). JeDeli natomiast poci?g ma zostaF wyprawiony w przeciwnym kierunku, odbierany jest sygna7 z linii transmisyjnej i uk7ad oczekuje na reakcj9 dyDurnego ruchu. MoDe równieD zostaF wydane polecenie specjalne AZK, inicjuj?ce awaryjn? zmian9 kierunku blokady. JeGli Dadne z powyDszych nie ma miejsca, sprawdzana jest poprawnoGF sygna7u odbieranego z linii transmisyjnej. Nieprawid7owa wartoGF wektora zmiennych wejGciowych powoduje przejGcie do stanu b79du.
DyDurny ruchu posterunku, który posiada blokad9 ustawion? na wyjazd, moDe j? zastopowaF, uniemoDliwiaj?c podanie sygna7u zezwalaj?cego (na przyk7ad w przypadku zamkni9cia toru szlakowego). W przypadku blokady zastosowanej na szlaku dwutorowym (gdy kaDdy tor posiada za7oDony kierunek zasadniczy) po przeje_dzie poci?gu kierunek powinien pozostaF ustawiony. Zwolnienie kierunku na stacji przyjmuj?cej poci?g moDe si9 odbyF z wykorzystaniem licznikowanego polecenia zwolnienia blokady. JeDeli natomiast uk7ad ma byF wykorzystany na linii jednotorowej, po wykryciu wjazdu poci?gu blokada powinna powróciF do stanu neutralnego. W tym celu naleDy uzupe7niF algorytm o funkcj9 wykrycia wjazdu poci?gu. JeGli przy utwierdzonym przebiegu wjazdowym zaj9ty zostanie pierwszy odcinek kontrolowany, uk7ad powinien oczekiwaF na zaj9cie drugiego odcinka. Po zaj9ciu drugiego odcinka kontrolowanego, aby dosz7o do samoczynnego zwolnienia spe7nione musz? zostaF nast9puj?ce warunki: zwolnienie pierwszego odcinka kontrolowanego, zwolnienie odcinka szlakowego, wyGwietlony sygna7 zabraniaj?cy na semaforze wjazdowym. Na kaDdym etapie detekcji wjazdu moDliwe jest równieD uDycie
polecenia zwolnienia blokady, gdyby w wyniku usterki urz?dze@ kontroli niezaj9toGci sekwencja dzia7ania odcinków kontrolowanych by7a b79dna.
Na podstawie szczegó7owego opisu wszystkich zak7adanych funkcji blokady stworzony zosta7 pe7ny algorytm dzia7ania. Nast9pnym etapem prac jest jego formalny zapis.
4.2. FORMALNY ZAPIS ALGORYTMU
Pierwszym krokiem jest zadeklarowanie zmiennych wejGciowych i wyjGciowych. Przyj9to, De zmienne wejGciowe oznaczane b9d? jako elementy wektora X, a zmienne wyjGciowe jako elementy wektora Y. Sk7adowe wektora X objaGnione zosta7y w tab. 1.
Tablica 1
Zestawienie sk+adowych wektora zmiennych wej6ciowych
Symbol
zmiennej Znaczenie Warto6ci
xwbl, xowb, xpzk, xzwb, xsto, xost, xazk
Polecenia: w7?czenia blokady, odwo7ania w7?czenia blokady, pozwolenia, zwolnienia kierunku,
zastopowania, odstopowania, awaryjnej zmiany kierunku
0 - Polecenie nie zosta7o wydane 1 - Polecenie zosta7o wydane
XL Sygna7 z linii transmisyjnej
000 - B7?d / brak po7?czenia 001 - Stan neutralny
010 - Kierunek ustawiony na wyjazd 011 - Awaryjna zmiana kierunku 100 - Kierunek ustawiony na wjazd xits, xit1, xit2 Kontrola zaj9toGci odcinków torowych 0 - Odcinek jest zaj9ty 1 - Odcinek jest wolny
xuwj, xuwy Kontrola utwierdzenia przebiegów wjazdowego i wyjazdowego 0 - Przebieg jest utwierdzony 1 - Przebieg nie jest utwierdzony
xkcw Kontrola sygna7u zabraniaj?cego na semaforze wjazdowym 0 - Sygna7 zabraniaj?cy nie jest wyGwietlony 1 - Sygna7 zabraniaj?cy jest wyGwietlony
Dla zmiennych wielobitowych zastosowano uzupe7niaj?cy zapis okreGlaj?cy wartoGF wektora w zapisie heksadecymalnym (np. XL(5) oznacza, De zmienna XL ma wartoGF
binarn? "101"), co pozwala na uproszczenie zapisu warunków logicznych.
Przekszta7cenie opisu s7ownego w algorytm polega na zidentyfikowaniu stanów, zmiennych i zaleDnoGci pomi9dzy nimi. Nast9pnie naleDy wybraF jedn? z dwóch metod zapisu algorytmu - schemat graficzny lub logiczny.
4.2.1. Graficzny schemat algorytmu
Zapis algorytmu przy pomocy schematu graficznego opiera si9 na przedstawieniu poszczególnych kroków w postaci klatek. WyróDniF moDna klatki operacyjne, zawieraj?ce stan wyjGF, oraz klatki warunkowe, w których wartoGF zawartego równania logicznego decyduje o wyborze kolejnego kroku. Rys. 2. przedstawia algorytm dzia7ania
projektowanego modu7u blokady zapisany przy uDyciu GSA.
!
Graficzny schemat algorytmu to metoda ch9tnie wykorzystywana przy opisie prostych problemów, g7ównie z uwagi na czyteln? postaF rysunkow?, zrozumia7? dla kaDdego. Taki zapis pozwala co prawda doGF 7atwo przeprowadziF statyczn? analiz9 dzia7ania uk7adu, jednak jego zapis wraz z wzrostem z7oDonoGci algorytmu staje si9 uci?Dliwy w tworzeniu i zajmuje duDo miejsca. PoniewaD do celów weryfikacji wykorzystaF moDna wspomaganie komputerowe, 7atwoGF analizy nie jest juD tak istotnym czynnikiem, waDniejsze zaG staje si9 wygodne tworzenie i przekszta7canie zapisu. Dlatego zastosowaF moDna równowaDny zapis w postaci schematu logicznego.
4.2.2. Logiczny schemat algorytmu
Logiczny schemat algorytmu to formalny zapis dzia7ania, ekwiwalentny do zapisu w postaci GSA, maj?cy jednak zwart?, matematyczn? form9 zamiast graficznej [13]. W tej metodzie algorytm zapisany jest w postaci ci?gu nast9puj?cych po sobie symboli. Stany (b9d?ce elementami zbioru Y) warunkuj? wartoGci zmiennych wyjGciowych zgodnie z przyj9tym kodowaniem. Zmienne wejGciowe (zbiór X) decyduj? o kolejnym wykonywanym kroku. JeGli sprawdzany warunek ma wartoGF logiczn? '1', wykonywana jest kolejna operacja (po prawej stronie). JeGli natomiast warunek jest równy '0', kolejny krok wskazywany jest przez strza7k9 skierowan? w gór9 o odpowiednim numerze. Takich strza7ek moDe byF w algorytmie wiele. Strza7ka skierowana w dó7 oznacza miejsce, od którego naleDy kontynuowaF realizacj9 algorytmu. Taka strza7ka wyst9puje tylko raz dla kaDdego numeru. Znak q oznacza bezwzgl9dny skok do miejsca wskazanego przez strza7k9 (warunek logiczny zawsze fa7szywy). PoniDej zestawiono uDywane symbole:
Yk – symbol wektora zmiennych wyjGciowych,
xk – symbol zmiennej wejGciowej,
Xk – symbol wektora zmiennych wejGciowych, Xk = (x1, x2, ..., xn),
i
– symbol sprawdzenia warunku, jeGli poprzedzaj?ce wyraDenie jest równe '1' to nast9pn? wykonywan? czynnoGci? jest kolejny symbol z prawej strony, jeGli zaG wartoGF wyraDenia to '0', wykonywany jest skok do miejsca oznaczonego numerem i,
i
! – symbol miejsca skoku o numerze i, strza7ka o takim numerze wyst9puje w algorytmie tylko raz,
i
" – symbol bezwzgl9dnego skoku (warunek zawsze fa7szywy).
#
$
#
$
#
$
#
$
1 2 4 7 1 9 2 1 3 2 9 (2) (1) (4) (1) 3 8 7 1 3 9 4 5 1 4 9 (1) (4) (1) (2) 5 8 6 10 5 9 6 1 (3) 1 (4) (1)N wbl its L azk L IWY owb tim L L
WY sto azk L its uwy L IWJ pzk L L
WJ L zwb it uwj L ZWJ L L Y x x X x X Y x x X X Y x x X x x X Y x X X Y X x x x X Y X X " " " " " ! % ! & ! % % ! ! & !
#
$
6 9 7 5 7 (2) (2) 8 3 8 9 7 8 9 10 6 11 10 9 (3) 1 2 (2) 11 6 6 11 9 2 1 (2) AZ LSTOP ost ERR azk L D zwb it L
D zwb it its kcw L Y X Y x Y x X Y x x X Y x x x x X " " " " " " ! ! ! ! ! % %
Nawet dla doGF prostego algorytmu zapis w postaci LSA jest prostszy w przekszta7caniu, niD reprezentacja graficzna. W miar9 wzrostu skomplikowania uk7adu róDnica ta b9dzie coraz bardziej widoczna.
Zapis formalny algorytmu przedstawia w sposób jednoznaczny sposób dzia7ania uk7adu, nie istniej? jednak narz9dzia pozwalaj?ce na wykorzystanie tej formy opisu bezpoGrednio w Grodowisku wspomagania komputerowego. MoDna natomiast wykorzystaF do tego celu zapis w postaci grafu stanów.
4.3. GRAF STANÓW AUTOMATU SKO)CZONEGO
Systemy sterowania ruchem kolejowym mog? byF modelowane przy pomocy automatu sko@czonego [1]. Automat sko@czony opisywany jest uporz?dkowan? pi?tk? A = <X, Y, Q, +, ,>, gdzie:
X - wektor zmiennych wejGciowych, Y - wektor zmiennych wyjGciowych, Q - stan wewn9trzny,
+ - funkcja przejGF, , - funkcja wyjGF.
Metod? jednoznacznego opisu automatu sko@czonego jest graf stanów. Jest to forma graficzna (podobnie jak graficzny schemat algorytmu), ma jednak t9 zalet9, De moDe byF 7atwo wykorzystana w Grodowisku wspomagania komputerowego, co zaprezentowane zostanie w dalszej cz9Gci pracy. Dla prostych przypadków moDliwe jest skonstruowanie grafu bezpoGrednio z opisu s7ownego. Wraz ze wzrostem z7oDonoGci uk7adu konieczne staje si9 skorzystanie poGrednio z formalnego zapisu algorytmu, jak zosta7o to wykonane w przypadku tego projektu.
Do przekszta7cenia algorytmu w graf stanów wykorzystaF moDna obie zaprezentowane formy zapisu. Konieczne jest zdefiniowanie zaleDnoGci pomi9dzy metodami. W przypadku zapisu algorytmu w postaci GSA proces ten polega na oznakowaniu stanów i utworzeniu tranzycji 7?cz?cych stany zgodnie z warunkami zapisanymi w klatkach warunkowych.
Wykonanie grafu na podstawie logicznego schematu algorytmu jest nieco prostsze. Dla kaDdej strza7ki skierowanej w dó7 (czyli dla kaDdego wiersza) stworzyF naleDy stan oznaczony tak, jak w LSA. Nast9pnie dla kaDdego warunku sprawdzanego w danym stanie
naleDy stworzyF tranzycj9, która prowadzi do stanu zgodnie z numerem strza7ki, a jej warunek logiczny tworzy zanegowane równanie ze schematu logicznego.
Rysunek 3 przedstawia graf stanów dla opracowanego algorytmu.
Rys. 3. Graf stanów
W tab. 2 zestawiono dodatkowo porównanie zastosowanych metod zapisu tranzycji. Nast9pnym etapem prac jest umieszczenie projektu w Grodowisku komputerowym, co pozwoli na wygenerowanie ostatecznej postaci formalnego zapisu algorytmu, czyli kodu j9zyka VHDL.
Tablica 2
Metody zapisu tranzycji
GSA LSA Graf stanów
1 1
A n B
Y x Y
! ! !
4.4. SPECYFIKACJA W J/ZYKU VHDL
Do specyfikacji algorytmu w j9zyku opisu sprz9tu wykorzystany zosta7 pakiet
Active-HDL firmy Aldec. Pakiet ten stanowi zintegrowane Grodowisko tworzenia w j9zykach
VHDL oraz Verilog, pozwala pracowaF w trzech edytorach. Edytor tekstowy HDE s7uDy do tworzenia bezpoGrednio w j9zyku, zapewniaj?c pomocne narz9dzia do automatycznego zarz?dzania sk7adni? i kontroli b79dów. Dwa pozosta7e narz9dzia to edytory graficzne, które generuj? kod j9zyka na podstawie wykonanej specyfikacji. S? to edytory FSM (w którym specyfikacj9 stanowi graf stanów) oraz BDE (który pozwala 7?czyF fragmenty projektu w schemat blokowy). W praktyce projekt wykonywany jest równolegle we wszystkich edytorach - elementy kombinacyjne w edytorze HDE, elementy sekwencyjne w edytorze FSM, a wszystkie 7?czone s? w ca7oGF w edytorze BDE.
Zasadniczy algorytm dzia7ania projektowanej blokady wyspecyfikowany zosta7 w edytorze FSM. Posiadaj?c graf stanów zaprojektowany w poprzednim rozdziale wystarczy przenieGF go w Grodowisko oprogramowania komputerowego, zapisuj?c zmienne i warunki logiczne zgodnie z zasadami wykorzystywanego j9zyka opisu sprz9tu. Wykonan? specyfikacj9 projektowanego algorytmu przedstawia rys. 4.
Specyfikacja wykonana w edytorze FSM sk7ada si9 z dwóch cz9Gci. Zasadniczy obszar projektu zawiera opis architektury uk7adu w postaci grafu stanów. Widoczne s?, oprócz stanów i tranzycji, warunki logiczne oraz wartoGci zmiennych wyjGciowych w kaDdym ze stanów. Dodatkowo moDliwe jest umieszczanie komentarzy objaGniaj?cych elementy grafu. Ponad grafem znajduje si9 pole opisuj?ce jednostk9 projektow?, na którym widoczne s? zadeklarowane zmienne wejGciowe i wyjGciowe. W przypadku zmiennych wielobitowych okreGlona jest teD szerokoGF wektora.
Edytor FSM oferuje szereg dodatkowych funkcji pozwalaj?cych na uproszczenie konstrukcji grafu. Symbolem trójk?ta oznaczony jest stan resetuj?cy, wskazuj?cy stan pocz?tkowy uk7adu. Zostanie on ustawiony niezw7ocznie po wykryciu wartoGci '1' na wejGciu reset. WartoGci zmiennych wyjGciowych przypisane do stanu pocz?tkowego obowi?zuj? jako domyGlne (jeGli nie przypisano innych) w pozosta7ych stanach.
PoniewaD do stanu ERR istnieje tranzycja z wielu stanów (po niespe7nieniu Dadnego z za7oDonych warunków), stan ten otrzyma7 atrybut stanu domyGlnego (Default State). Stany, z których nie istnieje przejGcie do stanu ERR (gdzie niespe7nienie Dadnego z warunków powinno spowodowaF pozostanie w danym stanie) otrzyma7y tranzycj9 z uDyciem warunku @else, który oznacza dowoln? wartoGF wektora zmiennych wejGciowych inn? niD istniej?ce tranzycje wychodz?ce ze stanu.
Na tranzycjach widoczne s? numery priorytetu, okreGlaj?ce kolejnoGF sprawdzania warunków logicznych zgodnie z zaprojektowanym algorytmem. Odpowiada to kolejnoGci klatek warunkowych w GSA lub sprawdzeniu warunku w LSA.
PoniewaD elementy algorytmu zaznaczone szarymi obszarami maj? zastosowanie tylko dla linii jednotorowych, moDna umieGciF je jako jeden element, który moDna 7atwo usun?F. Taki z7oDony element (stan hierarchiczny) zawiera w sobie kilka stanów, upraszczaj?c postaF grafu. Jego konstrukcja oraz reprezentacja na zasadniczej cz9Gci grafu widoczne s? na rys. 5.
Rys. 5. Stan hierarchiczny (zawartoGF i reprezentacja na g7ównym grafie)
Kolejnym elementem pozwalaj?cym na uproszczenie projektu jest stan opó_nienia. Powoduje on wstrzymanie wykonywania nast9pnej tranzycji przez okreGlon? liczb9 impulsów zegara. Zosta7 on wykorzystany w dodatkowym bloku, który powoduje powrót do stanu neutralnego w przypadku nie odebrania pozwolenia z s?siedniego posterunku przez okreGlony czas. Graf stanów tego bloku widoczny jest na rys. 6.
Rys. 6. Stan opó_nienia
Wszystkie zaprezentowane elementy po7?czone zosta7y w edytorze BDE, a nast9pnie wygenerowany zosta7 kod j9zyka VHDL. Tak przygotowany zapis formalny moDe byF nast9pnie zweryfikowany i przetestowany, co zaprezentowane zostanie w kolejnym rozdziale.
5. WERYFIKACJA
I
BADANIA
SYMULACYJNE
MoDliwoGF wykonania symulacji dzia7ania wyspecyfikowanego uk7adu jest zasadnicz? zalet? zastosowania pakietu wspomagania komputerowego. Wykorzystanie wbudowanego symulatora logicznego polega na przypisaniu wymusze@ do zmiennych wejGciowych (wymuszeniami mog? byF mi9dzy innymi zegary predefiniowane, sygna7y losowe, klawisze Hotkey) i badaniu odpowiedzi uk7adu. Prac9 modelu podczas symulacji obserwowaF moDna bezpoGrednio na grafach i schematach blokowych (graficznie) oraz na przebiegach symulacji. Pierwsza metoda pozwala weryfikowaF poprawnoGF sekwencji zmian stanów. Przebiegi czasowe symulacji umoDliwiaj? rejestrowanie stanu kaDdej zmiennej w dowolnie wybranej chwili.
W pierwszej kolejnoGci naleDy sprawdziF poprawnoGF specyfikacji algorytmu w j9zyku opisu sprz9tu. Proces ten nazywany jest weryfikacj? modelu. Weryfikacja umoDliwia sprawdzenie, czy przejGcia pomi9dzy stanami zachodz? przy zgodnych z algorytmem wzbudzeniach, oraz czy wartoGci zmiennych wyjGciowych w kaDdym ze stanów odpowiadaj? wartoGciom za7oDonym przez projektanta. Ten etap projektowania pozwala wyeliminowaF b79dy przypadkowe zwi?zane z tworzeniem specyfikacji. PoniewaD w miar9 rozbudowy uk7adu weryfikacja wykonywana r9cznie by7aby coraz trudniejsza, pakiet
Active-HDL umoDliwia wygenerowanie sekwencji wymusze@ (tzw. Testbench), która
pozwala na automatyzacj9 procesu. Rys. 7 przedstawia przebiegi symulacji podczas weryfikacji.
Rys. 7. Zapis automatycznej weryfikacji
Pozytywny wynik weryfikacji modelu stanowi punkt wyjGcia do przeprowadzenia symulacji dzia7ania blokady. Badania symulacyjne powinny obejmowaF sprawdzenie wszystkich funkcji zak7adanych dla urz?dzenia. Aby moDliwa by7a symulacja nie tylko dzia7ania pojedynczego modu7u, ale blokady liniowej jako ca7oGci, wykonany zosta7 model urz?dze@ na szlaku. Zawiera on dwa modu7y stacyjne blokady oraz elementy odzwierciedlaj?ce urz?dzenia stacyjne oraz medium transmisyjne. Specyfikacja modelu szlaku w edytorze schematów blokowych przedstawiona jest na rys. 8. MoDliwoGF tworzenia rozbudowanych struktur hierarchicznych jest niew?tpliw? zalet? opisywanej metody, pozwalaj?c? w pe7ni wykorzystaF moDliwoGci wspomagania komputerowego.
Program bada@ symulacyjnych powinien obejmowaF wszystkie funkcje, jakie zosta7y przewidziane dla projektowanego uk7adu. Na wykonanym modelu linii zosta7y wi9c zasymulowane typowe przejazdy poci?gów w obu kierunkach (zawieraj?ce w sobie procesy ustawienia oraz zwolnienia kierunku), oraz procedury obs7ugi awaryjnej (odwo7ania próby w7?czenia kierunku, zwolnienia ustawionego kierunku, awaryjnej zmiany kierunku). Podczas symulacji stany zmiennych wejGciowych ustawiane by7y zgodnie z rzeczywistym dzia7aniem urz?dze@ stacyjnych (odcinki kontrolowane, stany sygnalizatorów Gwietlnych) za pomoc? odpowiednio przypisanych przycisków Hotkey. Efektem symulacji s?, podobnie jak w przypadku weryfikacji modelu, przebiegi czasowe. Prac9 blokady moDna równieD obserwowaF na schematach blokowych i grafach poszczególnych elementów, uzyskuj?c pe7ny wgl?d w zachowanie si9 urz?dzenia (rys. 9).
Rys. 9. Podgl?d wartoGci zmiennych podczas symulacji
MoDliwe jest zatem sprawdzenie reakcji blokady na róDne kombinacje wymusze@ (odzwierciedlaj?ce rzeczywiste przypadki) juD na etapie tworzenia projektu. Rysunek 10 przedstawia fragment symulacji obs7ugi blokady. Okno podgl?du przebiegów symulacji umoDliwia wybór sygna7ów które b9d? wyGwietlane, a takDe ich odpowiednie wyróDnienie i opisanie. Widoczne s? zmienne odpowiadaj?ce za sygna7 taktuj?cy (CLK), sygna7y przesy7ane lini? transmisyjn? pomi9dzy posterunkami ruchu (BUS...), oraz zmienne przypisane do polece@ oraz wyjGF uk7adu.
Rys. 10. Stan hierarchiczny
Zapis przebiegów pokazuje zachowanie si9 uk7adu w przypadku próby w7?czenia kierunku przy braku kryterium niezaj9toGci odcinka szlakowego. UDycie polecienia wbl na stacji A nie powoduje wtedy nadania D?dania do stacji B, wydane musi zostaF polecenie specjalne awaryjnej zmiany kierunku na stacji B (po upewnieniu si9, De w istocie szlak jest wolny). Kierunek blokady zostaje wtedy ustawiony, jednak po uDyciu polecenia AZK blokad9 naleDy odstopowaF (polecenie ost). Odstopowanie powoduje pojawienie si9 zezwolenia na podanie sygna7u zezwalaj?cego na wyjazd ze stacji A (zmienna A_szw).
W podobny sposób zasymulowane zosta7y wszystkie moDliwe sytuacje kluczowe z punktu widzenia bezpiecze@stwa ruchu kolejowego. PoniewaD wszystkie opisane etapy specyfikacji oraz symulacji wykonywane s? w jednym Grodowisku wspomagania komputerowego, w przypadku wykrycia nieprawid7owoGci moDemy niezw7ocznie poprawiF specyfikacj9 i powtórnie dokonaF weryfikacji, bez potrzeby zmiany platformy projektowania. Dzi9ki temu moDemy mieF pewnoGF, De efekt specyfikacji dok7adnie odpowiada zamierzeniom projektanta. Do etapu tworzenia prototypu dociera wi9c model sprawdzony.
6. PODSUMOWANIE
Zaproponowana w artykule metoda specyfikacji urz?dze@ srk pozwala w jednoznaczny sposób przejGF przez proces tworzenia projektu od opisu s7ownego do kodu j9zyka opisu sprz9tu. Projektowanie odbywa si9 tu z wykorzystaniem wygodnych edytorów, pozwalaj?cych w pe7ni wykorzystaF moDliwoGci wspomagania komputerowego. Dzi9ki tak wykonywanej specyfikacji moDna zdecydowanie skróciF czas opracowywania modelu, poGwi9caj?c wi9cej czasu na dopracowanie koncepcji. Zastosowanie symulatorów
logicznych pozwala juD na etapie projektu przetestowaF dzia7anie uk7adu w dowolnie wybranych warunkach. Po zbadaniu poprawnoGci wykonania specyfikacji moDliwa jest dalsza praca nad modelem, prowadz?ca do powstania prototypu. Wszystkie te etapy mog? byF przeprowadzone w jednym Grodowisku wspomagania komputerowego, co sprawia, De zaproponowana metoda specyfikacji urz?dze@ srk spe7nia wymagania stawiane poszukiwanej platformie opisowej systemów przeznaczonych dla kolei.
Bibliografia
1. D?browa-Bajon M.: Podstawy sterowania ruchem kolejowym. OWPW, Warszawa 2007.
2. Fokkink W., Groote J., Hollenberg M., van Vlijmen B.: LARIS 1.0 Language for Railway Interlocking Specifications. CWI, 2000.
3. Hlavatý T., Pveuwil L., Štypán P.: Case Study: Formal Methods in Development and Testing of Safety Critical Systems: Railway Interlocking System. EUROMICRO 2001.
4. Kalisz J. (red.): J9zyk VHDL w praktyce. WKi|, Warszawa 2002.
5. 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. 6. Kawalec P., Koli@ski D.: Modelowanie interlocking'u z zastosowaniem j9zyka opisu sprz9tu. Logistyka
6/2010, Pozna@, 2010, str. 1329 – 1337.
7. Kawalec P., Koli@ski D.: Zastosowanie j9zyka VHDL do badania z7oDonych sieci zestykowych. Pomiary Automatyka Kontrola, vol. 54, nr 8 –2008, Wydawnictwo PAK, Warszawa, 2008, str. 529 – 531.
8. Kawalec P., RDysko M.: Komputerowo wspomagana specyfikacja funkcji zaleDnoGciowych urz?dze@ srk. Technika Transportu Szynowego, |ód_, 9/2012, str. 1605 – 1615.
9. Kawalec P., RDysko M.: Zastosowanie j9zyków opisu sprz9tu do specyfikacji urz?dze@ srk. Logistyka 4/2012, Pozna@, str. 351 – 358.
10. Mikulski M.: Mechaniczne urz?dzenia zabezpieczenia ruchu kolejowego. WKi|, Warszawa 1983. 11. Pasierbi@ski J., Zbysi@ski P.: Uk7ady programowalne w praktyce. WKi|, Warszawa 2002. 12. Piela S.: Samoczynna blokada liniowa typu Eac.
13. Traczyk W.: Uk7ady cyfrowe. Podstawy teoretyczne i metody syntezy. WNT, Warszawa 1982.
14. Zaj?czkowski A., Kalici@ska K., Olendrzy@ski W.: Elektryczne urz?dzenia zabezpieczenia ruchu kolejowego. Urz?dzenia stacyjne. WKi|, Warszawa 1976.
15. WTB-E10 Wytyczne techniczne budowy urz?dze@ sterowania ruchem kolejowym w przedsi9biorstwie PKP.
FORMALALGORITHMCONSTRUCTIONMETHODFORRAILWAYTRAFFIC
CONTROLDEVICES
Summary: The article presents a method of railway traffic control algorithm specification using formal
description and computer aided design. The review of currently used description methods of railway traffic control devices and systems indicates that the method which could ensure a uniform platform for description of all kinds of discrete control systems does not exist. Most of currently used description methods do not allow the use of computer support at the stage of specification and verification. It is shown that application of hardware description languages 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 computer support in the form of logic simulators. On the examplary specification of one-section line block operation algorithm in VHDL, both the possibilities of
Active–HDL package as well as the process of computer aided specification and verification of the designed
system are presented.
