EP0796779B1 - Method for the control and the safety of a guided transport system - Google Patents

Abstract

The method involves storage in formal language of a model of all foreseeable network states and events. Type-related dynamic data are represented in the form of Petri nets or their derivatives, and example-related static track network data in the form of double-vertex graphs. A first algorithm computes all possible sequence states and prevents triggering of a verifiable event when a forbidden state is involved. A second algorithm is brought in when an unacceptable event occurs, triggering verifiable events when these reduce the expected number of consequential forbidden states.

Description

The invention relates to a method according to the preamble of Claim 1.

Such a procedure is from the dissertation from M. Montigel "Modeling and ensuring dependencies in Railway safety systems ", submitted in 1994 to the Federal Technical University, Zurich (DISS.ETH No. 10776) known.

It is intended to control and secure the methods used today Track-guided transport systems, especially railway networks replace and also planning and economic use transport systems in a completely new way support.

The types of solutions used for system control and - Securing is based on track elements with neighboring relationships, provided with train speed data to form a Route either via geographic circuits with each other linked and then saved, or accordingly a prepared route that represents the route to be set List one after the other on their occupancy status and their current Setting checked and, if necessary, after switching to a predetermined location, be secured.

These solutions are unsatisfactory in terms of treatment of the system using formal methods. The construct track element, by which there are relatively many basic types is still too complex for this.

The above The dissertation therefore sees the representation of the rail network with the help of colon graphs, which are compared to a Representation with simple directed graphs has the advantage that there is no unnatural marking of a direction of travel (which is the case with Track triangles and turning loops lead to problems), and that topological peculiarities can be better taken into account For example, hairpin bends on switches are not possible from the start are, therefore do not have to be excluded.

In the dissertation mentioned at the beginning, the system Railway protection as a distributed, discrete event system understood that with the help of formal languages as logical Data model can be reproduced, with individual data areas are represented as stated at the beginning.

The method proposed there is based on close dependencies and initially refrains from formulating Safety conditions. It becomes a model of the states and Events of the system that developed the formulation of allowed illegal states and events on a local basis, i.e. no distant dependencies need to be considered. The requirements for the security system are not direct described, but the behavior of the system including the itself vehicles moving in it is modeled as such, like if there was no security level. The in the Security level to implement security conditions then result as consequences of the modeled System Properties.

Instead of, as usual, in the security system Implementing security conditions explicitly becomes one Representation of all relevant for operational security held states and events developed, especially those that are considered inadmissible for security reasons become. Events are in controllable and split uncontrollable. An event is called exactly then controllable if freedom in any system state exists to prevent it from arriving, otherwise it means Event uncontrollable.

At runtime, the security system always contains an image of everyone States of the overall system as well as the rules as from the current one State all subsequent states can be calculated. in the another is an algorithm (so-called eunomic algorithm) implemented that every time a controllable event to be triggered, the set of all possible, by following subsequent states caused by uncontrollable events calculated and then examined whether they have one or more contains illegal states.

In order to be able to represent the large number of states in the system in a space-saving manner, a distributed representation with Petri nets was chosen. In this way, 2 ⁿ states can be represented with n binary digits or conditions. The algorithm mentioned above, which checks the admissibility of a controllable event, does not really calculate the amount of subsequent states that can be reached in an uncontrollable manner, since this would be far too extensive, but only clarifies the derivability of each individual location or event individually (not in combination ). It can be shown that every achievable state or event can be derived in the above sense, so that an inadmissible state cannot be reached if the corresponding points cannot be derived.

• Schrittweises Entwickeln eines formalen Modells der Sicherungsebene des Transportsystems auf der Ebene eines Systemtyps (z.B. System für ein bestimmtes Transportsystem oder eine bestimmte Bahnverwaltung) in Form eines Predicate/Transition-Netzes. Dieses Modell beschreibt die Zustände und Zustandsübergänge der Sicherungsebene und ist unabhängig von den zu sichernden Gleisnetzen. Wenn für dasselbe oder ein ähnliches Transportsystem bereits früher ein Modell erarbeitet wurde, können die dort definierten allgemeinen Systemeigenschaften für das neue Modell übernommen werden.
• Erstellen der Spezifikationen der zu sichernden Gleisnetze (Daten der Systemexemplare)
• Durchführen eines automatisierten sogenannten Entfaltungsprozesses mittels Entfaltungstools:
  • Syntax-, Typen- und Plausibilitätsprüfung des Typ-Modells
  • Vorbereitung des Typ-Modells für den eigentlichen Entfaltungsprozess
  • Erzeugung von symbolischen Schnittstellen für die von der Sicherungsebene abhängigen Ebenen (Steuerungsebene, Hardware-Interface-Ebene etc.)
  • Herstellen eines interpretier- oder ausführbaren formalen Modells für die Systemexemplare (eigentliche Entfaltung):
  • Für jeden allgemein beschriebenen Zustand und
  • Zustandsübergang im abstrakten Typmodell werden alle konkreten Instanzen gesucht, die sich aus den Exemplardaten ergeben. Resultat ist ein Condition/Event-Netz, daß das entsprechende Systemexemplar beschreibt. Jeder Knoten des Netzes besitzt einen eindeutigen Namen, der sich aus dem Namen des entsprechenden abstrakten Knotens und den Namen der konkreten Objekte des Gleisnetzes zusammensetzt, auf die er sich bezieht.
  • Überprüfen des formalen Exemplar-Modells mit einem Laufzeitsystem für Condition/Event-Netze. Dieses System enthält eine Implementation des o.g. Eunomischen Algorithmus, der die Zulässigkeit von kontrollierbaren Ereignissen überwacht. In der o.g. Dissertation wurden die von der Sicherungsebene abhängigen Ebenen (Außenanlage, Steuerungsebene etc.) mit interaktiven Tools simuliert. Die Sicherungsebene kann sowohl auf hohem Abstraktionsniveau (Simulation von Zügen) wie auch auf dem Detailniveau (Betrachtung einzelner Knoten des Condition/Event-Netzes) simuliert werden.

The development process of a security system is as follows in the procedure described in the dissertation:

• Step-by-step development of a formal model of the security level of the transport system at the level of a system type (e.g. system for a specific transport system or a specific railway administration) in the form of a predicate / transition network. This model describes the states and state transitions of the security level and is independent of the track networks to be secured. If a model has already been developed for the same or a similar transport system, the general system properties defined there can be adopted for the new model.
• Creation of the specifications of the track networks to be secured (data of the system copies)
• Carrying out an automated so-called unfolding process using unfolding tools:
  • Syntax, type and plausibility check of the type model
  • Preparation of the type model for the actual development process
  • Generation of symbolic interfaces for the levels dependent on the security level (control level, hardware interface level etc.)
  • Creating an interpretable or executable formal model for the system copies (actual development):
  • For every generally described condition and
  • State transition in the abstract type model is searched for all concrete instances that result from the instance data. The result is a condition / event network that describes the corresponding system copy. Each node of the network has a unique name, which is made up of the name of the corresponding abstract node and the names of the concrete objects of the rail network to which it refers.
  • Checking the formal copy model with a runtime system for condition / event networks. This system contains an implementation of the above-mentioned eunomical algorithm, which monitors the admissibility of controllable events. In the above-mentioned dissertation, the levels dependent on the security level (outdoor facility, control level, etc.) were simulated using interactive tools. The security level can be simulated both at a high level of abstraction (simulation of trains) and at the level of detail (consideration of individual nodes of the condition / event network).

The in the above Procedures reproduced in thesis still contains no concept for route monitoring and for different others common in railway control systems today Control concepts.

It is therefore an object of the invention to have a function in the known Integrate procedures that include monitoring an initially for allowed path considered permissible.

This object is achieved by the specified in claim 1 Features resolved.

By observing the entry of so-called "normally not events to be assumed ", i.e. events such as Rail breaks or loss of the end position for switches whose Taking into account every journey in a track network from the start would make inadmissible, with the help of the additional, so-called reverted eunomic algorithm can have dangerous consequences avoid from such events in many cases or at least reduce their probability of occurrence.

Developments of the method according to the invention are in the Subclaims specified and relate to others to be included Control concepts.

So claims 2 and 3 concern the inclusion of Concept of speed in the control system, claim 3 concerns the treatment of train operations and the interpretation of section assignments.

Claim 4 relates to the representation of transport units Help of sequences of occupied track sections.

Subject of claim 5, finally, are the use of new ones Transport units and the detection of train separations by means of Occupancy and free notifications of track sections.

The method according to the invention is to be described below with reference to Embodiments and detailed with the help of four figures to be discribed.

Fig. 1 -

den Aufbau der verwendeten Datenverarbeitungsanalge,

Fig. 2 -

schematisch einen Überblick über die Erstellung der Sicherungsebene,

Fig. 3 -

die Bewegung der Spitze eines Zuges in einem mit Doppelpunktgraphen dargestellten Gleisnetz,

Fig. 4 -

eine schematische Darstellung der Systemreaktion bei Eintritt eines unkontrollierbaren, normalerweise nicht anzunehmenden Ereignisses.

The figures show:

Fig. 1 -

the structure of the data processing system used,

Fig. 2 -

schematically an overview of the creation of the security level,

Fig. 3 -

the movement of the tip of a train in a track network represented by a colon graph,

Fig. 4 -

a schematic representation of the system reaction when an uncontrollable, normally unlikely event occurs.

In Fig. 1 is the structure of the data processing system with the Help the method according to the invention is carried out, shown. The figure shows two levels, which - separately from each other - the control or the securing of the outdoor area forming track network including the existing switches, Signals, signaling devices and the one using the track network Trains serve. The main functions of the security level and the control level are shown in the figure.

Fig. 2 gives an overview of the creation of the data for the Assurance level. As can be seen from the figure, first a general Petri network e.g. a predicate / transition network, the one includes formal specification of the system type from which over the network available information is created and based on consistency and correct Checked syntax. It will then, along with the special Track topology data, e.g. in the form of colon graphs can be present with the help of a suitable deployment tool unfolds, whereby a special Petri net, e.g. on Condition / event network that creates the data for the Contains security level and in as a runtime system Algorithm (so-called eunomic algorithm) is applicable, the before controllable events all made possible by these Grid changes examined for their admissibility and at too anticipated inadmissible events triggering the controllable event prevented.

The following exemplary embodiments specifically describe the Creation of the security level and the application of the so-called reverted eunomical algorithm.

I. Creation of the security level 1. Create a formal specification of the system type from a informal.

• Transitionen
• Prädikate
• Kanten
• abhängige Transitionen

The description language are predicate / transition networks. The specification includes:

• transitions
• predicates
• edge
• dependent transitions

Example:

Movement of a Zugspitze over the track network (general specification, independent of topology), according to Figure 3

Specification language constructs

An edge is defined that leads from the predicate pred to the transition trans or vice versa. In the first case pred is a precondition, in the second a postcondition of trans. During the development process, solutions for condition are sought for each transitional copy of trans. Each such solution then creates a copy of the edge of this type in the Petri net specially made for a track topology.
Edgtype values:

Pair of dependent events, the admissibility of the arrival of transname1 depends on whether transname2 in the Petri network othernet also is permissible.

2. Syntax and consistency check

• Korrekte Syntax
• Entspricht <transtype> und <predtype> einem vordefinierten Typ?
• Sind die Typendefinitionen der Variablen konsistent?
• Sind <trans> und <pred> in allen Kantendefinitionen korrekt definiert?

It is checked:

• Correct syntax
• Does <transtype> and <predtype> correspond to a predefined type?
• Are the type definitions of the variables consistent?
• Are <trans> and <pred> correctly defined in all edge definitions?

3. Creation of the data of the track topology

Colon graphs are used to represent the track topology

4. Unfolding

For each transition type, all suitable variable assignments are taken from the Object set of the track topology so that the condition <transcondition> becomes true. Each such variable assignment results in a transition instance. For each Transition specimen are searched for all edges so that the edge conditions are true with the corresponding variable assignment.

5. Runtime system

The runtime system leads the special to the corresponding track topology belonging to Petri nets. It contains an implementation of the EUNOMIC Algorithm,

II. Example of a formal specification of a security level

III. Reverted EUNOMIC algorithm

Algorithm that is started when an uncontrollable event that cannot be assumed arrives and looks for an emergency dependency in the set of controllable events that prevents the occurrence of impermissible follow-up events. The algorithm is formulated in Objective-C.

For example :

In the example shown in Figure 4, the switch loses its defined end position (uncontrollable, but usually not event to be assumed). This threatens a state in which the Zugspitze of the approaching train is on a switch, that has no defined end position (edg_crash). To do this prevent, the above algorithm is started. He examines the Predecessor set of the event "edg_crash" and finds the Emergency dependency "reset_signal - head". Then that will Event "reset_signal triggered that the main signal on hold throws.

Claims (5)

1. Method of controlling and protecting the operation of any randomly configured track-guided transport system with the aid of a data processing system in which a model of all the states and events occurring in the transport system is stored in a formal language, in such a way that dynamic data that change owing to events occurring, insofar as they can be assigned to a track element type in a way independent of the track network, in the form of Petri nets of high abstraction level, insofar as they can be assigned in the track network concretely to existing track elements, are represented in the form of nets derived from said Petri nets, and static data valid for every system state, insofar as they can be assigned to a track element type in a way independent of the track network, in the form of predicates or invariants, insofar as they can be assigned in the track network concretely to existing track elements, are represented in the form of topography element data, and in which data processing system an algorithm is available that, prior to initiating a controllable event, calculates all the possible consequential states from the current state of the system and prevents the initiation if one or more inadmissible states are found among the calculated consequential states, characterized in that an uncontrollable event whose occurrence cannot be expected from the outset is defined as a normally unexpected event, and in that, during the checking of the admissibility of a controllable event, it is not expected that a normally unexpected event occurs, in that an additional algorithm is started if, after establishing the admissibility of the controllable event, a normally unexpected event occurs, in that, by means of the additional algorithm, the set of all the states achievable as a result of consequences of uncontrollable events is examined, proceeding from the actual system state generated by the occurrence of said event, in regard to whether a state designated as inadmissible occurs among them or the preliminary conditions for the occurrence of an event designated as inadmissible are fulfilled, and in that, if this applies, the set of all the events or controllable events designated particularly for this case are investigated in regard to whether the system state can be altered by its initiation in such a way that the set of the previously calculated, achievable inadmissible states or events designated as inadmissible is reduced and that, if that is the case, the appropriate controllable events are initiated.
2. Method according to Claim 1, characterized in that speed data in the form of data tuples are assigned to the topography element data assigned to the track elements concretely existing in the track network, which speed data contain, in addition to valid maximum speeds, also data from which an achievable delay can be achieved with maximum brake use, in that the speeds valid at a track element, insofar as they are not redetermined, are calculated recursively or iteratively from data that have been assigned previously to traversed track element in the respective direction of travel, and in that the calculated speed data are used for establishing maximum speeds valid in the system.
3. Method according to Claim 2, characterized in that the topography element data assigned to the track elements have the form of double-point diagrams and the data tuples containing the speed data are assigned to the points or edges of said double-point diagrams.
4. Method according to any of the preceding claims, characterized in that the track segments of the track network are fitted with track idle status indicators, in that a continuous sequence of occupied segments is interpreted as a transport unit moving in the track network and the direction of travel is deduced from the order of the new occupations or idle status indications and in that an individual incorrect idle status indication does not change the assumed size of the transport unit.
5. Method according to Claim 4, characterized in that an individual occupation of a segment is interpreted, in the case of valid idle status indication for all the adjacent segments, as a new transport unit initially having two heads and no tail, in that the occupation of a segment situated, seen in the direction of travel, behind the tail of an existing transport unit is interpreted as a change in the direction of travel of the transport unit or as a separate part of the transport unit starting to move backwards, and in that, in both cases, the original tail of the transport unit is converted into a head in the system model.

Images