Project duration: 1 October 1995 to 30 September 1998

Project partners: University of Bremen, ELPRO LET GmbH Berlin

Financing by: BMBF and University

The scientific results of the Oldenburg working group in this joint project concern the combination of methods for the specification and development of distributed communicating systems with real-time requirements, a Moby/PLC tool as part of the UniForM Workbench for the development of PLC software and the processing of case studies defined by the industrial partner ELPRO for safe railway control in the field of traffic control technology.

While the process algebra CSP (Communicating Sequential Processes) is well suited for the description of communicating processes, Object-Z is an object-based specification method for data, states and their transformation. CSP is embedded in a mature and theoretically well-studied semantics for distributed, communicating systems. Inspired by Oldenburg's preliminary work in the ESPRIT basic project ProCoS, in particular the specification language MIX developed there, C. Fischer succeeded in combining both methods in the specification language CSP-OZ.

In CSP-OZ, process aspects are described in CSP and data aspects in Object-Z. The simple semantics based on the failures-divergence model of CSP are particularly noteworthy. This means that the refinement concept of CSP and the tool support provided by the model checker FDR (Failure-Divergence-Refinement) can be used for CSP-OZ.

The Duration Calculus (DC for short) was introduced into the UniForM project to specify time-critical aspects of computer systems. The DC is intended as a high-level specification language for formalising requirements. At the lowest level of implementation, programmable logic controllers (PLCs for short) were to be considered in the UniForM project, as these are widely used in control and automation technology.

One of the challenges of the UniForM project was to build a bridge from the duration calculus to PLCs so that the correctness of PLC software with regard to the requirements set in the duration calculus can be proven. H. Dierks found out that the behaviour of PLCs can be represented very well in an abstract way by a new real-time automaton model, so-called PLC automata. The semantics of PLC automata describe the cyclical mode of operation of PLCs, consisting of three phases: Reading in the sensor values, calculating the new state and outputting parts of this state to the actuators. The cycle time is the decisive parameter for the exact temporal behaviour of PLCs and therefore of PLC automata.

The semantics of PLC automata were specified with the help of the duration calculus. Therefore, PLC automata represent a combination of the concept of the PLC with the DC. In addition, equivalent semantics were developed on the basis of timed automata. This made it possible to establish a connection to external model checkers UPPAAL and KRONOS for the automatic verification of real time properties.

With the involvement of a student project group led by H. Fleischhack and J. Tapken and several Diplom theses, the Moby/PLC tool for working with PLC automata was developed, which includes the following components:

• a graphical editor for entering PLC automata,
• a simulator for networks of PLC automata,
• a compiler for generating code in the PLC programming language ST (Structured Text),
• an algorithm for statically analysing real-time conditions
• conversion procedures for the external tools UPPAAL and KRONOS for model checking of real-time requirements,
• a synthesis procedure for generating PLC automata from a subset of the Duration Calculus, the DC-Implementables.

Moby/PLC was presented at CeBIT'98.

In coordination with the industrial partner ELPRO, the case study Safeguarding single-track lines (SES) was initially selected. This concerns the correct traffic control of trams on single-track sections. PLCs were chosen as the methodological approach.

The customer requirements, in this case from the Berliner Verkehrs-Gesellschaft (BVG), were used as the basis for analysing the requirements for the SES. In Oldenburg, these requirements were analysed by H. Dierks for part of the case study independently of the ELPRO and specified with the help of PLC automata. This specification was then presented to ELPRO and experiences were exchanged.

Once the requirements analysis had been completed, a network of 14 PLCs was developed in the design phase using the Moby/PLC tool. Moby/PLC was used to simulate the entire automation network simultaneously. In addition, important correctness statements (e.g. ``A maximum of one direction of travel is always shown in green'') were proven. Real-time requirements arose for individual PLC machines, e.g. for the components for filtering bouncing sensor signals. The control system in the form of the network of PLC automata was then translated into 700 lines of PLC source code in the ST (Structured Text) programming language using the compiler developed in Oldenburg and validated on a PLC simulator.

After completion of the SES case study, ELPRO presented a new case study of a current tram control system ("Jena Steinweg") as a challenge to the PLC automation approach. SES and Jena Steinweg are similar in terms of routing, but in the latter case study considerably more tram movements are permitted. This interlocking function accounts for the complexity of the case study. Fortunately, it turned out that this case study could also be handled in the Moby/PLC tool.