Wyniki wyszukiwania - BazTech

1

Wybrane zagadnienia formalizacji systemów srk

Zabłocki W.

Zeszyty Naukowo-Techniczne Stowarzyszenia Inżynierów i Techników Komunikacji w Krakowie. Seria: Materiały Konferencyjne

|

2015

|

Nr 3(107)

147--156

PL

W publikacji przedstawiono wybrane zagadnienia opisu formalnego na przykładzie opisu funkcji sprzeczności. Zamieszczony przykład opisu formalnego został poprzedzony rozważaniami dotyczącymi opisów nieformalnych i półformalnych w ogólnym odniesieniu do procesu projektowania systemu srk i tworzenia dokumentacji systemu. Proces tworzenia poprawnych i pełnych opisów n-p-f staje się istotny z punktu widzenia warunków bezpieczeństwa. Opracowane dokumenty i formy opisu systemu srk stają się bazowymi dokumentami dowodu bezpieczeństwa. Metoda opisu formalnego sprzeczności dróg przebiegów odwołuje się do analizy właściwości obiektów uczestniczących w drogach przebiegów, tj. uwzględnia szczegółowo właściwości obiektów drogi jazdy, drogi ochronnej i obiektów ochronnych. Zaproponowany przykład metody formalizacji pozwala określić wystarczające warunki sprzeczności. Jednakże proponuje się zachować tablicę zależności z wykazanymi sprzecznościami dróg przebiegów jako podstawową formę klasycznego opisu półformalnego.

EN

The publication presents selected issues of formal description on the example of the function description contradictions. Included example on formal description was preceded by considerations relating to informal and semi-formal descriptions in relation to the overall system design process ATC and system documentation. The process of creating the correct and complete, informal, semi-formal, formal descriptions becomes important from the point of view of safety requirements. Background documents and forms of SRK description of the system are treated as the base documents of proof of safety. The method of formal description of contradiction routes refers to the analysis of properties of objects involved in routes, taking into account the detailed properties of objects route (drive path, overlap path and protective object). The proposed formalization of such methods allows you to specify sufficient conditions of contradictions. However, it is proposed to keep the interlocking board according to the disclosed contradiction routes as the basic form of the classical semi-formal description.

2

Zagadnienie sprzeczności i wykluczeń specjalnych w technice srk

Zabłocki W.

Zeszyty Naukowo-Techniczne Stowarzyszenia Inżynierów i Techników Komunikacji w Krakowie. Seria: Materiały Konferencyjne

|

2014

|

Nr 2(104)

399--406

PL

W publikacji przedstawiono specyfikację dokumentacji wymaganej przy opracowywaniu założeń i projektowaniu komputerowych systemów sterownia ruchem. Istotnym zagadnieniem projektowania takich systemów jest automatyzacja utworzenia tablicy zależności z wykazem sprzecznych dróg przebiegów. Zalgorytmizowanie wyznaczania sprzeczności dróg przebiegów wymaga opracowania metody pozwalającej formalizować relacje sprzeczności. Podstawą formalizacji są szczegółowe właściwości obiektów drogi przebiegu i ich analiza zgodna z zasadami bezpieczeństwa, ze szczególnym uwzględnieniem funkcji sprzeczności dróg przebiegów. W projektowaniu komputerowych systemów sterowania powstaje dylemat: czy wyznaczenie funkcji sprzeczności spełnia także wymagania dotyczące sprzeczności dróg przebiegów o wykluczeniach specjalnych. Zaproponowana metoda formalizacji sprzeczności pozwala określić wystarczający warunek sprzeczności, który odnosi się także do wykluczeń specjalnych. Jednakże proponuje się zastosowanie klasycznej tablicy zależności z wykazanymi sprzecznościami dróg przebiegów i wykluczeniami specjalnymi. Oznaczenie wykluczeń specjalnych będzie stanowić dodatkowy czynnik bezpieczeństwa systemu srk.

EN

The publication presents the specifications of the documentation required in developing of the assumptions and designing computer systems for traffic control. Another important issue is the design of such systems is to automatically create an array according to a list of conflicting routes. Algorithmization of determination of contradictions routes requires to develop a method to formalize the relations conflict. The basis of formalizing are detailed properties of the route objects and analysis consistent with the safety regulations, with particular emphasis on routes contradiction function. In the design of computer control systems arises dilemma whether design of contradiction functions also meets the requirements for routes contradiction with the special exclusion. The proposed method of contradiction formalization allows to determine sufficient condition for conflict, which also applies to the special exclusions. However, it is proposed to apply the classic array interlocking to the disclosed conflicts of routes and special exclusions. Marking of special exclusions will be an additional safety factor of the train control system (ATC).

3

Metodyka budowy komputerowych systemów srk

Maciejewski M., Zabłocki W.

Zeszyty Naukowo-Techniczne Stowarzyszenia Inżynierów i Techników Komunikacji w Krakowie. Seria: Materiały Konferencyjne

|

2011

|

Nr 96, z. 158

289--305

PL

W publikacji przedstawiono ogólne założenia metody tworzenia komputerowych systemów srk. Podstawą metody projektowania systemu srk jest strategia oparta na analizie systemowej uwzględniającej cykl V oraz podejście COTS. Treść publikacji zawiera opisy wybranych etapów projektowania należących do cyklu V. Opisy obejmują własności systemu srk i podstawy metody formalizacji opartej na modelu systemu srk nawiązującym do układu przełączającego (automatu), w którym zostają wyróżnione automaty składowe umożliwiające odwzorowanie funkcji sterowania. Podstawą analizy pracy automatów jest specyfikacja sygnałów oraz wyznaczenie funkcji przejść uzupełnione schematami grafów przejść. Rezultatem powyższej metodyki projektowania jest wypracowana metoda pozwalająca tworzyć bezpieczne komputerowe systemy sterowania ruchem.

EN

The general assumptions for the method of computer system for atc construction have been presented in the paper. The basis of the method of atr system designing is the strategy resulting from system analysis including V cycle and COTS approach. The descriptions of some designing stages that belong to V cycle have been given. The descriptions contain the atr system properties and the basis of formalization method. The basis of machines work analysis is specification of signals and definition of transfer function completed with schemes of transfer graphs. The result of mentioned above methodology of designing is the method allowing to create computer systems for traffic control.

4

Synteza funkcji należnościowych stacyjnego systemu srk

Zabłocki W.

Zeszyty Naukowo-Techniczne Stowarzyszenia Inżynierów i Techników Komunikacji w Krakowie. Seria: Materiały Konferencyjne

|

2009

|

Nr 91, z. 149

523-548

PL

W artykule przedstawiono zarys metody formalizacji systemu srk. Podstawą formalizacji są własności drogi przebiegu analizowane zgodnie z zasadami bezpieczeństwa ze szczególnym uwzględnieniem funkcji sprzeczności dróg przebiegów. Zaproponowana metoda formalizacji definiuje uporządkowane statyczne i dynamiczne struktury danych oraz relacje. Struktury informacji są podstawą konstrukcji relacji, które pozwalają sformułować funkcje i inne relacje zależnościowe systemu srk, a w tym i funkcje sprzeczności dróg przebiegów. Opis formalny relacji i funkcji zależnościowych umożliwia zredagowanie równań zależnościowych warunkujących algorytmizację sterowania. Rezultatem powyższych badań jest formalny (matematyczny) model systemu srk. Model i zbudowany na jego podstawie symulator stanowią narzędzia badawcze, które pozwalają nie tylko wnioskować o systemie srk, a także tworzyć system rzeczywisty.

EN

The outline of the method of rail traffic control systems have been presented in the paper. The features of routing analysed according to safety rules including in particular functions of contradictory functions are the basis of formalisation. The proposed formalisation method defines static and dynamic ordered database structures and relations. The information structures are the basis for creating the relations that allow defining functions and other interlocking relations of rail traffic control facilities including functions of contradictory routings. The formal description of interlocking relations and functions allows defining interlocking equations qualifying control algorithmisation. The result of research is formal (mathematic) model of rail traffic control system. Model and the simulator, constructed basing on it, compose the research tools used for drawing conclusions on rail traffic control facilities and for creating real facilities.

5

Modelowanie stacyjnych systemów sterowania ruchem kolejowym

Zabłocki W.

Prace Naukowe Politechniki Warszawskiej. Transport

|

2008

|

z. 65

3-180

PL

Efektywne i bezpieczne sterowanie ruchem kolejowym na stacji jest realizowane przez złożone systemy srk. Jedną z podstawowych metod badania systemu srk jest metoda modelowania prowadząca do badań symulacyjnych z zastosowaniem symulatora komputerowego. Metoda modelowania wpisuje się w schemat przyjętej metody badawczej. W pracy określono ogólne i szczegółowe cele modelowania systemu srk. Podstawowym celem modelowania jest wnioskowanie o zachowaniu systemu rzeczywistego srk, który odwzorowuje zadania sterowania. Na podstawie opisu nieformalnego powstał opis formalny systemu srk, reprezentowany przez model systemu sterującego. Model systemu sterującego MSS obejmuje model statyczny - MSTA i model dynamiczny MDYN. Informacje modelu statycznego i dynamicznego są odwzorowywane przez dwie struktury statyczne i dwie struktury dynamiczne. Struktury statyczne zawierają informacje: o własnościach obiektów w drogach przebiegu na stacji, wartości funkcji sprzeczności dla dróg przebiegów wyróżnionych na stacji. Struktury dynamiczne tworzą rejestr przebiegów i stanów przebiegów występujących na stacji i przechowują wartości sygnałów odwzorowujących stan urządzeń zewnętrznych na stacji. Model systemu srk złożony jest zbioru automatów odpowiadających drogom przebiegów i obiektom. Każdy przebieg odpowiadający konkretnej drodze przebiegu jest traktowany jako skończony automat sekwencyjny o określonych wejściach i wyjściach oraz własnym stanie wewnętrznym. Podobnie opisywane są również obiekty - urządzenia zewnętrzne. Statyczne własności drogi przebiegu i dynamiczne własności przebiegu stają się podstawą formalizacji zależności, ze szczególnym uwzględnieniem funkcji sprzeczności dróg przebiegów. Własności drogi przebiegu i przebiegu pozwalają sformułować relacje modelu systemu sterującego. Do relacji tych należą relacje zależnościowe, które wyrażają: warunki sprzeczności lub niesprzeczności dróg przebiegów, predyspozycje przebiegowe, kryteria zwalniania oraz pozostałe relacje opisujące zmiany stanu systemu srk. Na podstawie relacji i funkcji zależnościowych tworzone są równania zależnościowe, wyznaczające wartości sygnałów zmiennych stanu przebiegów i obiektów oraz sygnałów wyjściowych obiektów do zewnętrznych urządzeń wykonawczych tych obiektów. Zasady formalizacji systemu srk zostały dostosowane do koncepcji cyklicznego przetwarzania równań zależnościowych dla każdego przebiegu. Stan procesu zachodzącego w systemie i stany obiektów są wczytywane na początku każdego cyklu przetwarzania. Po wczytaniu sygnałów od obiektów następuje przetwarzanie informacji o przebiegach i poleceniach do obiektów, zakończone wyznaczeniem nowych stanów przebiegów i obiektów oraz generacja˛ poleceń - sygnałów wyjściowych obiektów do urządzeń wykonawczych obiektów. Przeprowadzone eksperymenty symulacyjne dla zadanych ograniczeń i przykładowo przyjętego układu torowego potwierdzają, że koncepcja opisu formalnego systemu oraz przygotowane na podstawie tego opisu oprogramowania symulatora systemu srk są poprawne i spełniają˛ warunek przetwarzania w czasie rzeczywistym. Uzyskane wyniki modelowania i symulacji są istotne m.in. z następujących względów: - opracowany model systemu srk staje się formą standaryzacji opisu takiego systemu, - opracowany opis formalny stwarza podstawy do: ▪ zastosowania nowoczesnych metod projektowania oprogramowania, uwzględniających język UML lub metody specyfikacji formalnej, np. logiki modalnej, ▪ projektowania oprogramowania rzeczywistego systemu zależnościowego.

EN

Effective and safe automatic train control (ATC) at station is conducted by means of composed ATC systems. One of the basic methods for testing an ATC system is the modelling method leading to simulation research using a computer simulator. The modelling method fits into a frame of adopted research method. General and detailed modelling goals of ATC system have been defined in chapter 1.3 and in chapter 6. The basic purpose of modelling is to draw conclusions about the behaviour of a real ATC system that reflects controlling tasks. On the basis of an informal description, a formal description of ATC system has been made represented by the control system model. The control system model MSS includes a static model - MSTA and a dynamic model - MDYN. Informations fed by the static and dynamic models is reflected by two static structures and two dynamic structures. The static structures include data about: properties of objects in route at the station, values of conflict function for routing processes identified at the station. The dynamic structures establish a register of the routing processes and statuses of processes taking place at the station and store values of signals reflecting the status of external devices at the station. The ATC system model consists of a set of automatons corresponding to routes and objects. Each routing process corresponding to a specific routing process is treated as finite sequential automaton of defined inputs and outputs and its own internal state. Objects - external devices are also described in a similar way. Static properties of the route and dynamic properties of the routing process become a basis for formalisation of dependence with a special focus on the route conflict function. Properties of the routes and the routing process itself allow to formulate relations of the control system model. The relations include dependence relations that express conditions of conflict or lack of conflict between routing processes, process predispositions, slowing down criteria and other relations describing changes in ATC system status. On the basis of relations and dependence functions, dependence equations are created, thus determining values of signals of variables of the processes and object states and output signals of objects to external executive devices of the objects. The ATC system formalisation rules have been tailored to the concept of cyclical processing of dependence equations for each process. The state of a process ongoing in the system and states of objects are fed at the beginning of each processing cycle. Processing of processes and orders data to objects commence after the signals from objects have been fed and they finish with determination of new states of the processes and objects as well as generation of orders - output signals of the objects to the executive devices of the objects. The conducted simulative experiments for the assumed limitations and the adopted track system confirm that the concept of a formal description of the system and software programs, prepared on the basis of that description, for the ATC system simulator, is correct and meets the requirement of real-time processing. The obtained modelling and simulation results are essential inter alia for the following reasons: - the prepared model of ATC system becomes a form of standardisation of description of such a system, - the prepared formal description constitutes the basis for: ▪ application of modern methods of software designing, taking into consideration UML language or formal specification methods, e.g. modal logic, ▪ designing software of the real dependence system.