Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 7

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
PL
W artykule przedstawiono propozycję formalnej metody specyfikacji złożonych funkcji zależnościowych w systemach srk. Opisana metoda opiera się na podejściu geograficznym, umożliwiającym wykorzystanie zbudowanych elementów dla dowolnego układu torowego. Zastosowanie algorytmów do opisu działania pozwala na intuicyjne przejście od elementarnych warunków, opisanych w języku naturalnym, do zapisu formalnego oraz kodu języka VHDL. Zaprezentowane zostały również możliwości weryfikacji otrzymanych algorytmów.
EN
The paper presents several problems concerning the interlocking logic design process in modern railway traffic control systems. This issue is increasingly difficult in implementing new functions and adapting systems to new market requirements. For easy and clear transition from the verbal operation description to the formal notation in HDL language, the algorithmic approach was introduced. Universal input and output alphabets proposed in the paper allow convenient variable identification. The rules for decomposing the system into objects and algorithms are described (Fig. 1). Since the method is based on the geographical approach, the set of designed elements is universal and can be used for any track layout. Using the logical algorithm scheme (2) to describe the functionalities allows one to intuitively transform the elementary conditions in a natural language to a formal notation and finally to the VHDL code (Fig. 4). Verification possibilities of the described method are also presented. Using the Active-HDL integrated design environment it was possible to analyze the created algorithms on many hierarchical levels. Beginning from the algorithm level (proving the correctness of the transition to the finite-state machine graph), through the object level (Fig. 5a, showing the complex interlocking functions) to the whole interlocking logic (Fig. 5b, allowing verification of the design using the interlocking table), all of the performed simulations proved correctness of the specification.
EN
The paper presents a modelling method for complex interlocking functions in railway traffic control systems. The method is based on the geographical approach, which allows to use the created elements for any track layout. Specification and verification of the designed algorithms was performed in computer-aided design environment. The use of algorithms to describe the functions allowed to intuitively transform the elementary conditions in verbal description into formal notation and finally the VHDL code.
PL
W artykule przedstawiono propozycję sformalizowanej metody specyfikacji złożonych funkcji zależnościowych w systemach sterowania ruchem kolejowym. Opisana metoda opiera się na podejściu geograficznym, umożliwiającym uniwersalne wykorzystanie zbudowanych elementów dla dowolnego układu torowego. Zaprezentowane zostały możliwości specyfikacji i weryfikacji otrzymanych algorytmów w środowisku komputerowego wspomagania prac projektowych. Zastosowanie algorytmów do opisu działania pozwala na intuicyjne przejście od elementarnych warunków opisanych w języku naturalnym do zapisu formalnego i ostatecznie kodu języka VHDL.
PL
W artykule przedstawiona została problematyka weryfikacji logiki zależnościowej współczesnych systemów sterowania ruchem kolejowym. Złożoność zagadnienia rośnie w ostatnich latach w wyniku wielu istotnych czynników, takich jak konieczność zapewnienia interoperacyjności systemów, czy tendencja do obejmowania sterowaniem z jednej nastawni coraz większych obszarów. Utrudniona staje się więc manualna analiza poprawności działania projektowanych systemów. W związku z tym do weryfikacji zaproponowane zostało wykorzystanie nowoczesnego, zintegrowanego pakietu programistycznego Active-HDL. Na przykładzie zestawu równań zależnościowych opracowanego w języku VHDL przedstawione zostały możliwości pakietu w zakresie weryfikacji projektu.
EN
This paper presents a formal method for railway interlocking logic verification. After decomposing the railway control system into objects and algorithms, interlocking functions were described using formal methods. This allowed the use of integrated design environment - Active-HDL, for verification of the whole design and building VHDL code as a final description. Various methods of manual and automated simulation are presented, showing the capabilities of the described design and verification method.
PL
W artykule przedstawiono propozycję stworzenia metody formalnego zapisu algorytmów działania urządzeń zabezpieczenia ruchu kolejowego z wykorzystaniem grafów przejść automatów skończonych. Przegląd stosowanych obecnie metod opisu urządzeń srk wskazuje, że nie istnieje jednolita platforma opisu wszelkiego rodzaju dyskretnych układów sterowania. Większość stosowanych metod nie pozwala na wykorzystanie wspomagania komputerowego na etapie specyfikacji i weryfikacji tego typu układów. Na przykładzie stworzonego modelu przykładowego urządzenia zostało pokazane, że zastosowanie do tego celu grafów przejść pozwala stworzyć kompletną platformę specyfikacji algorytmów działania urządzeń srk, pozwalając dodatkowo na statyczną i dynamiczną weryfikację poprawności opisu z wykorzystaniem języków opisu sprzętu.
EN
The article presents a method of railway traffic control algorithm specification using finite-state machine diagrams. The review of currently used description methods of railway traffic control devices and systems indicates that a complete platform for description of all kinds of discrete control systems does not exist. It is shown that application of FSM diagrams 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 hardware description languages and logic simulators. On the exemplary operation algorithm of point module, both the possibilities of Active–HDL package as well as the process of computer aided specification and verification of the designed system are presented.
5
Content available remote Metoda tworzenia formalnego zapisu algorytmów działania urządzeń srk
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.
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.
PL
W artykule przedstawiono zagadnienia wspomaganej komputerowo specyfikacji urządzeń srk z wykorzystaniem języków opisu sprzętu. Przegląd stosowanych obecnie metod opisu urządzeń i systemów srk wskazuje, że nie istnieje metoda, która mogłaby zapewnić jednolitą platformę opisu wszelkiego rodzaju dyskretnych układów sterowania. Dodatkowo 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 specjalizowanego układu.
EN
The article presents several issues concerning computer aided specification of railway traffic control devices using hardware description languages. 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. In addition, the majority of description methods currently used do not allow the use of computer support at the stage of specification and verification of operation algorithms of this type of systems. 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 example of specification of one-section line block operation algorithm in VHDL, both the possibilities of Active–HDL package as well as the process of computer supported specification and verification of the designed specialized system are presented.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.