Narzędzia help

Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
first last
cannonical link button

http://yadda.icm.edu.pl:80/baztech/element/bwmeta1.element.baztech-cb409ae1-aa1f-4a6d-a710-c35281660e04

Czasopismo

Pomiary Automatyka Kontrola

Tytuł artykułu

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

Autorzy Kawalec, P.  Koliński, D. 
Treść / Zawartość
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, pka@wt.pw.edu.pl
autor Koliński, D.
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.
Kolekcja BazTech
Identyfikator YADDA bwmeta1.element.baztech-cb409ae1-aa1f-4a6d-a710-c35281660e04
Identyfikatory