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

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.

---

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.