Weryfikacja równań zależnościowych z wykorzystaniem symulatorów logicznych na przykładzie zastosowania pakietu Active-HDL

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.

---

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.