Metoda tworzenia formalnego zapisu algorytmów działania urządzeń srk

• Autorzy: Kawalec P. , Rżysko M.

Warianty tytułu

EN

Formal algorithm construction method for railway traffic control devices

• Języki publikacji: PL

Abstrakty

PL

W artykule przedstawiono problemy formalnego zapisu algorytmów działania urządzeń zabezpieczenia ruchu kolejowego oraz wspomaganej komputerowo specyfikacji tych algorytmów z wykorzystaniem języków opisu sprzętu. Przegląd stosowanych obecnie metod opisu urządzeń srk wskazuje, że nie istnieje metoda, która mogłaby zapewnić jednolitą platformę opisu wszelkiego rodzaju dyskretnych układów sterowania. Większość stosowanych metod opisu nie pozwala na wykorzystanie wspomagania komputerowego na etapie specyfikacji i weryfikacji algorytmów działania tego typu układów. Zostało pokazane, że zastosowanie do tego celu języków opisu sprzętu tworzy jednolitą platformę specyfikacji i weryfikacji urządzeń srk, pozwalając dodatkowo na statyczną i dynamiczną weryfikację poprawności opisu z wykorzystaniem wspomagania komputerowego w postaci symulatorów logicznych. Na przykładzie specyfikacji algorytmu działania jednoodstępowej blokady liniowej w języku VHDL zaprezentowane zostały zarówno możliwości pakietu Active-HDL, jak i proces wspomaganej komputerowo specyfikacji i weryfikacji projektowanego układu.

EN

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.

Słowa kluczowe

PL

język VHDL; blokada liniowa; sterowanie ruchem kolejowym; ruch kolejowy

EN

VHDL; line block; railway traffic control; railway traffic

• Wydawca: Oficyna Wydawnicza Politechniki Warszawskiej
• Czasopismo: Prace Naukowe Politechniki Warszawskiej. Transport
• Rocznik: 2013
• Tom: z. 100
• Strony: 91--108
• Opis fizyczny: Bibliogr. 15 poz., rys., tab.

Twórcy

autor

Kawalec P.

• Politechnika Warszawska, Wydział Transportu

autor

Rżysko M.

• Politechnika Warszawska, Wydział Transportu

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., Přeučil L., Štěpán P.: Case Study: Formal Methods in Development and Testing of Safety Critical Systems: Railway Interlocking System. EUROMICRO 2001.
• 4. Kalisz J. (red.): Język 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 języka opisu sprzętu. Logistyka 6/2010, Poznań, 2010, str. 1329-1337.
• 7. Kawalec P., Koliński D.: Zastosowanie języka VHDL do badania złożonych sieci zestykowych. Pomiary Automatyka Kontrola, vol. 54, nr 8, 2008, Wydawnictwo PAK, Warszawa, 2008, str. 529-531.
• 8. Kawalec P., Rżysko M.: Komputerowo wspomagana specyfikacja funkcji zależnościowych urządzeń srk. Technika Transportu Szynowego, Łódź, 9/2012, str. 1605-1615.
• 9. Kawalec P., Rżysko M.: Zastosowanie języków opisu sprzętu 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.: Układy programowalne w praktyce. WKiŁ, Warszawa 2002.
• 12. Piela S.: Samoczynna blokada liniowa typu Eac.
• 13. Traczyk W.: Układy 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 przedsiębiorstwie PKP.