Correct System Design Group

Moby/PLC

Designing Distributed Real-Time Control Programs with PLC-Automata

Safe system control

Serious failures of rail-bounded traffic systems like tram or railway are often caused by complex unmanageable control systems. It is for that reason, that technology is moving from centralized systems to collections of simple distributed components which are cooperating with each other. Hence, in the future, there will be fewer and fewer interlockings, but level crossings, switches, etc. will have their own control parts. These will communicate with the respective parts of neighbouring systems, with control panels in the trains, and with location systems like GPS, thus controlling the flow of traffic.In analogy, hardware components of future traffic control systems consist of simple modules like programmable logic controllers (PLCs). For designers of control systems, it will be possible to automatically verify safety as well as liveness properties of the (simple) components. On the other hand, typical problems of distributed systems as deadlock or breakdown of part of the system, have to be taken into account.

How Moby/PLC may help

Figure 1: Components of the Moby/PLC-System At this point, the Moby/PLC-System enters the game by supporting the development of distributed real-time control programs for PLCs. First, a system is modelled as a network of PLC-Automata, a graphical programming language with real-time extensions. Then, the design steps through a cycle exploring the behaviour of the model by simulation or by applying special analysis algorithms, and extending, changing, or refining the model appropriately. By the use of real-time model-checker it is even possible to perform a formal verification whether the design fulfills a certain (real-time) property.

Finally, control programs for the involved PLCs are generated automatically from the system specification. Note, that the PLC-Automaton model takes into account also the real-time requirements of the system. Figure 1 shows the basic structure of Moby/PLC.

Securing a single-track line segment (SLS)

Consider a segment where two lines converge. The control system has to prevent trains from passing through the single track segment in opposite directions at the same time. In addition, it should recognize faulty action of an engine driver or of the sensors and react accordingly. The SLS is shown schematically in Figure 2.

There are three sensors for each direction: 'Entry Sensor' (ES), 'Critical Section Sensor' (CS), and 'Leave Sensor' (LS). The region between ES and CS is the wait-segment. Also, there is a signal for each direction, showing

'Stop', if no train is in the wait-segment or if an error occurs.
'DemandStop', if there is a train in the wait-segment but has no permission to pass.
'Go', if passing in this direction is allowed.

The control strategy consists of giving permission to pass alternately to the directions. Figure 3 shows a network of PLC-Automata modelling the SLS control system (right part) and the automaton for a filter component (left part).
Figure 3: PLC-Automata network for the SLS

Figure 3: PLC-Automata network for the SLS

Visualization using VRML97 and Java

Figure4: 3D-Visualization of the SLS One possibility to see if a PLC program works properly, is to implement this program on a real PLC and let it run. Yet, simulation may be more feasible in many cases. Therefore, a three dimensional model of an SLS was built using VRML97 for geometric description of the 3D world and Java classes for controlling and communication. This scenario is connected to the PLC Simulator of the MOBY/PLC system via socket communication. Trains moving across the sensors give input to the PLC-Automata that are simulated. Their computations are given back to control the signals at the railway.

Where MOBY/PLC comes from

The MOBY/PLC-system has been developed within the Correct System Design group of the department of computing science at the university of Oldenburg. It is part of the UniForM project (Universal workbench for Formal Methods), which is run jointly by working groups within the universities of Bremen and Oldenburg (IEKOS) and by INSY GmbH, Berlin, and which is supported by the BMBF (federal ministry of education and research). The implementation of the system has been based on the Moby Class Library, which has also been developed in Oldenburg.

Publications concerning Moby/PLC can be found on the Moby/PLC page of the Correct System Design group's web-server. A beta version of a tutorial can be found here.

Contacts

Henning Dierks Hans Fleischhack Josef Tapken	Department of Computing Science C.v.O. University of Oldenburg D-26111 Oldenburg

phone:	+49 441 / 798-2411 or -3121
fax:	+49 441 / 798-2965

email:	moby@theoretica.informatik.uni-oldenburg.de

Download:	Order Moby/PLC by email for free.