Correct Real-Time Software for Programmable Logic Controllers - Correct System Design: Recent Insights and Advances - page 346

Constraint

Requirements

Diagrams

Synthesis

Model

Visualisation

Checking

Automaton-

Editor

Specifications

Simulator

Analysis

Algorithms

Compiler

ST-Code

Programs

PLC-Code

Fig. 7. Architecture of Moby/PLC

{ algorithms for translating PLC-Automata into timed automata in order to be
able to use UPPAAL [4,25] and KRONOS [6] for model checking of additional
real-time properties [10].

the case study Single Track Control has been tackled by
H. Dierks. Starting point were the informal requirements of the customer, in
this case the Berlin Trac Company. To deal with the safety, functional and
time critical parts of the requirements, an architectural plan for the control
software was developed identifying a number of logical components like lters,
counters, drive controller, error detection and trac light actuators. Then for
each of these components the corresponding requirements were formalised using
DC implementables (corresponding to a subset of Constraint Diagrams).
From these formalised requirements corresponding PLC-Automata were syn-
thesised for each component yielding a network of 14 PLC-Automata. Real-time
properties were relevant for some of these automata, in particular for the lters
for stuttering sensors as discussed in the Sections 4 and 5. Using

Using Moby/plc

this
network could be checked by simulation. Additional correctness properties were
proven, for example that it is never the case that the trac lights of the two
opposite directions show the Go signal at the same time. The PLC-Automata
network was then compiled into an ST program with 700 lines of code for exe-
cution on a single PLC. The program was again validated using a commercially
available PLC simulator.

Moby/plc