Correct System Design Group
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
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
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.
|last update: 2001/01/16 by Henning Dierks © 2000|