Zastosowanie wspomagania komputerowego w specyfikacji i weryfikacji formalnych opisów funkcji zależnościowych

• Autorzy: Kawalec P. , Koliński D.

Warianty tytułu

EN

Computer-aided specification and verification of formal description for interlocking functions

• Języki publikacji: PL

Abstrakty

PL

Wykorzystując rachunek macierzowy i teorię automatów, zaproponowano metodę formalnego zapisu funkcji zależnościowych realizowanych w systemach sterowania ruchem kolejowym (srk). Metoda ta stała się podstawą wspomaganej komputerowo specyfikacji tych funkcji w językach opisu sprzętu HDL. Zaproponowana metoda pozwala naintuicyjne przejście od formalnego opisu w postaci macierzy do grafów przejść automatów skończonych w edytorze FSM. Przytoczono wyniki weryfikacji w postaci przebiegów czasowych, na grafie przejść oraz na schemacie blokowym.

EN

The paper presents a formal specification method of interlocking functions in railway traffic control systems. The method utilizes matrix calculus and the automata theory. After defining the set of automaton internal states (9), the transition matrixes (16) and transition priorities matrixes, describing the conditions checking order (17), were developed. The obtained general mathematical description of interlocking functions defines a method for determining control functions based on input data, so it can be assumed that the control algorithms for interlocking functions were defined. The developed method was then used as a basis for computer aided specification of these functions in hardware description languages (HDL). The intuitive transition from the matrix-based formal description to the finite-state machine graph in FSM editor (Fig. 1) is the advantage of the proposed method. Verification of the created interlocking functions can be performed on waveforms (Fig. 2), on the FSM graph (Fig. 3) and on the hierarchical block diagram (BDE) (Fig. 4). This specification and verification process was used to create all possible 39 interlocking functions for 10 object types of the railway interlocking system. The specification and verification results proved the correctness of the developed interlocking function execution algorithms. Obtaining the description of the functions in VHDL language is an additional advantage of the proposed method, which allows automatic synthesis, implementation and execution of these functions in FPGA devices.

Słowa kluczowe

PL

sterowanie ruchem kolejowym; zależności; funkcje zależnościowe

EN

railway traffic control; interlocking; interlocking functions

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2014
• Tom: R. 60, nr 10
• Strony: 829--831
• Opis fizyczny: Bibliogr. 7 poz., rys.

Twórcy

autor

Kawalec P.

• Politechnika Warszawska, Wydział Transportu, Koszykowa 75, 00-662 Warszawa

autor

Koliński D.

• Egis Poland Sp. Z O.O., Puławska 182, 02-670 Warszawa

Bibliografia

• [1] Apuniewicz S.: Układy przekaźnikowe w automatyce zabezpieczenia ruchu kolejowego. WPW Warszawa, 1969.
• [2] Dąbrowa-Bajon M.: Podstawy sterowania ruchem kolejowym. Funkcje, wspomagania, zarys techniki. Wydanie drugie poprawione. Oficyna Wydawnicza Politechniki Warszawskiej, Warszawa, 2007 r.
• [3] Kawalec P.: Analiza i synteza specjalizowanych układów modelowania i sterowania ruchem w transporcie. Politechnika Warszawska, Prace Naukowe – Transport, Oficyna wydawnicza Politechniki Warszawskiej, Warszawa, 2009 r.
• [4] Koliński D.: Formalny opis funkcji zależnościowych systemów srk dla współczesnych posterunków ruchu. Politechnika Warszawska, Prace Naukowe – Transport, z. 86, Oficyna Wydawnicza Politechniki Warszawskiej, Warszawa, 2012, str. 35 – 52.
• [5] Koliński D.: Metoda specyfikacji i weryfikacji funkcji zależnościowych w systemach sterowania ruchem kolejowym. Rozprawa doktorska, Oficyna Wydawnicza Politechniki Warszawskiej, Warszawa, 2013.
• [6] Lewiński A.: Problemy oprogramowania bezpiecznych systemów komputerowych w zastosowaniach transportu kolejowego. Politechnika Radomska, Monografie Nr 49, Radom, 2001 r.
• [7] Zabłocki W.: Modelowanie stacyjnych systemów sterowania ruchem kolejowym. Politechnika Warszawska, Prace Naukowe – Transport, z. 65, Oficyna Wydawnicza Politechniki Warszawskiej, Warszawa, 2008 r.