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

9 Conclusion

In this paper we showed how ideas from the theory of real-time systems can be
used in an application area from the industrial practice: the design of railway
signalling systems based on Programmable Logic Controllers.
Our approach is in contrast to current industrial practice where software is
produced directly using languages like ST or of a lower level of abstraction and
then tested extensively to catch errors. Constraint Diagrams and PLC-Automata
allow for a more abstract and clearer view on the controller under design and
enable a formal verication of real-time properties.
Future research is concerned with the automatic verication (model checking)
of real-time properties for PLC-automata or more general real-time systems with
reaction times.

Acknowledgements. The work described in this paper is motivated by my par-
ticipation in the projects ProCoS ( Provably Correct Systems [17]) and UniForM
( Universal Workbench for Formal Methods [23]). I am indepted to H. Dierks,
C. Dietz, H. Fleischhack and J. Tapken for their work on various aspects of the
approach to real-time design described in this paper.

References

1. R. Alur, D. Dill. A theory of timed automata. Theoret. Comput. Sci. , 126, 1994,
283{235.
2. R. Alur, G.J. Holzmann, D. Peled. An analyzer for message sequence charts. In:
T. Margaria and B. Steen (Eds.), Tools and Algorithms for the Construction
and Analysis of Systems . LNCS 1055 (Springer-Verlag, 1996) 35{48.
3. R.J.R. Back. Renement calculus, part II: parallel and reactive Programs. In
J.W. de Bakker, W.P. de Roever and G. Rozenberg (Eds.), Stepwise Renement
of Distributed Systems { Models, Formalisms, Correctness . LNCS 430 (Springer-
Verlag, 1990) 67{93.
4. J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, W. Yi. Uppaal {atool
suite for automatic verication of real-time systems. In: Proc. 4th DIMACS
Workshop on Verication and Control of Hybrid Systems .NewBrunswick,New
Jersey, Oct. 1995.
5. T. Bienmuller, J. Bohn, H. Brinkmann, U. Brockmeyer, W. Damm, H. Hungar,
P. Jansen. Verication of Automotive Control Units. This volume.
6. C. Dawsa, A. Olivero, S. Tripakis, S. Yovine. The tool Kronos. In: R. Alur,
T.A. Henzinger, E.D. Sontag (Eds.), Hybrids Systems III { Verication and
Control . LNCS 1066 (Springer-Verlag, 1996).
7. H. Dierks. PLC-automata: a new class of implementable real-time automata. In:
M. Bertran and T. Rus (Eds.), Transformation-Based Reactive Systems Devel-
opment . LNCS 1231 (Springer-Verlag, 1997) 111{125. (Revised version to appear
in TCS)
8. H. Dierks. Synthesising controllers from real-time specications. In: Tenth In-
ternational Symposium on System Synthesis (IEEE CS Press, September 1997)
126{133.