Wyniki wyszukiwania - BazTech

1

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

Kawalec P., Koliński D.

Pomiary Automatyka Kontrola

|

2014

|

R. 60, nr 10

829--831

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.

2

Komputerowo wspomagana specyfikacja funkcji zależnościowych urządzeń srk w językach opisu sprzętu

Kawalec P., Rżysko M.

TTS Technika Transportu Szynowego

|

2012

|

R. 19, nr 9

1605--1614, CD

PL

W artykule omówiona została koncepcja wykorzystania języków opisu sprzętu do specyfikacji funkcji zależnościowych urządzeń sterowania ruchem kolejowym. Przegląd stosowanych rozwiązań pokazuje, że nie istnieje metoda opisu zapewniająca jednolitą platformę specyfikacji dyskretnych układów sterowania w kolejnictwie. Obecnie wykorzystywane metody nie oferują również możliwości statycznej i dynamicznej weryfikacji wykonanego układu. Proces projektowania przy użyciu proponowanej metody zaprezentowany został na przykładzie specyfikacji algorytmu działania pojedynczego modułu dla geograficznego systemu zależnościowego, tworzonego w języku VHDL. Zastosowanie symulatorów logicznych w procesie weryfikacji projektu pozwoliło na wykonanie symulacji potwierdzających poprawność działania modelu. Na podstawie tak wykonanej specyfikacji pokazano zalety wykorzystania wspomagania komputerowego w postaci wszechstronnego pakietu przeznaczonego do tworzenia w językach HDL.

EN

This paper presents several issues concerning computer aided specification of railway interlocking functions using hardware description languages. The review of currently used methods shows that none of them can provide a uniform design platform for railway applications, capable of static and dynamic verification of the design. The proposed design process is shown on an exemplary specification of a geographical interlocking module algorithm, written in VHDL. With the use of logic simulators it was possible to verify correctness of the description. The article presents various advantages of utilizing both hardware description languages and computer aided design software.

3

Wybrane problemy tworzenia funkcji i równań zależnościowych w systemach srk

Maciejewski M., Zabłocki W.

Prace Naukowe Politechniki Warszawskiej. Transport

|

2010

|

z. 72

87-100

PL

W publikacji przedstawiono wybrane problemy dotyczące metody tworzenia funkcji i równań zależnościowych na podstawie równań stanu opisujących system srk jako układ przełączający. Analiza systemu srk jako układu przełączającego pozwala wyróżnić w strukturze tego układu szereg automatów składowych odwzorowujących przebiegi, jak i obiekty sterowane. Do opisu tych automatów zastosowano równania stanu. Metoda ta umożliwiła sformułowanie funkcji i równań zależnościowych, które można zastosować do celów algorytmizacji. Ponadto zastosowanie tej metody pozwala zbadać własności tych automatów a tym samym i systemu srk.

EN

In the publication a method of creating the function and interlocking equations was presented on the basis of equations of the state describing the ATC system as the switching machine. Analysis of the ATC system as the switching machine lets single the row of automaton in the structure of this system as components reflecting of the rout process, as controlled objects. Equations of the state were used to the description of these machines. This method enabled to formulate the interlocking function and equations whom it is possible to apply to purposes of the algorithmization. Moreover applying this method allows to examine properties of these automaton hence and of ATC system. The required property of these automaton is among others their observability.

4

Interlocking functions of ATC station system

Zabłocki W.

Archives of Transport

|

2008

|

Vol. 20, iss. 4

89-108

EN

The paper presents a method for formalising and determining the value of interlocking function in a context of static and dynamic framework, containing information about train routing conflict. The information framework is an element necessary for description of relations in traffic controI systems at the station, as well as for creating control functions. The publication also presents a new method of defining ATC system and creating its model.

PL

W publikacji omówiono metodę formalizacji funkcji sterowania, a następnie na podstawie zaproponowanych statycznych i dynamicznych struktur informacji przedstawiono sposób określania wartości funkcji zależnościowych. Struktury informacji są także niezbędne do określania wartości funkcji sprzeczności dróg przebiegów i tworzenia równań zależnościowych. Ponadto w publikacji przedstawiono nowy sposób definiowania systemu SRK i metodę tworzenia jego modelu.