Zastosowanie grafów przejść automatów skończonych do opisu algorytmów działania urządzeń srk

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.

---

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.