×

zbMATH — the first resource for mathematics

PLC-automata: A new class of implementable real-time automata. (English) Zbl 0954.68085
Summary: We introduce PLC-automata as a new class of automata which are tailored to deal with real-time properties of Programmable Logic Controllers (PLCs). These devices are often used in industrial practice to solve controlling problems. Nevertheless, PLC-automata are not restricted to PLCs, but can be seen as a model for all polling systems. A semantics in an appropriate real-time temporal logic (duration calculus) is given and an implementation schema that fits the semantics is presented in a programming language for PLCs. A case study is used to demonstrate the suitability of this approach. We define several parallel composition operators, and present an alternative semantics in terms of timed automata for which model-checkers are available.

MSC:
68Q45 Formal languages and automata
Software:
Kronos; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] R. Alur, C. Courcoubetis, D. Dill, Model-checking for real-time systems, 5th Annu. IEEE Symp. on Logic in Computer Science, IEEE Press, New York, 1990, pp. 414-425. · Zbl 0769.68088
[2] Alur, R.; Dill, D.L., A theory of timed automata, Theoret. comput. sci., 126, 183-235, (1994) · Zbl 0803.68071
[3] R. Alur, T. Henzinger, E. Sontag (Eds.), in: Hybrid Systems III, Lecture Notes in Computer Science, vol. 1066, Springer, Berlin, 1996.
[4] Bengtsson, J.; Larsen, K.G.; Larsson, F.; Pettersson, P.; Yi, Wang, Uppaal – a tool suite for automatic verification of real-time systems, (), 232-243
[5] Bosscher, D.; Polak, I.; Vaandrager, F., Verification of an audio control protocol, (), 170-192
[6] J. Bowen, C.A.R. Hoare, H. Langmaack, E.-R. Olderog, A.P. Ravn, ProCoS II: A ProCoS II Project Final Report, Chapter 3 Number 59 in Bulletin of the EATCS, European Association for Theoretical Computer Science, June 1996, pp. 76-99.
[7] Daws, C.; Olivero, A.; Tripakis, S.; Yovine, S., The tool kronos, (), 208-219
[8] Dierks, H., PLC-automataa new class of implementable real-time automata, (), 111-125 · Zbl 0954.68085
[9] H. Dierks, Synthesising controllers from real-time specifications, in: 10th Internat. Symp. on System Synthesis, IEEE Computer Society, New York, September 1997, pp. 126-133, short version of [11].
[10] H. Dierks, Comparing model-checking and logical reasoning for real-time systems, in: Workshop Proc. of the ESSLLI’98, 1998, pp. 13-22.
[11] Dierks, H., Synthesizing controllers from real-time specifications, IEEE transac. comput.-aided design integrated circuits systems, 18, 1, 33-43, (1999)
[12] Dierks, H.; Dietz, C., Graphical specification and reasoningcase study generalized railroad crossing, (), 20-39
[13] H. Dierks, A. Fehnker, A. Mader, F.W. Vaandrager, Operational and logical semantics for polling real-time systems, in: Ravn, Rischel (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science, vol. 1486, Lyngby, Denmark, Springer, Berlin, September 1998. pp. 29-40, short version of [14].
[14] H. Dierks, A. Fehnker, A. Mader, F.W. Vaandrager, Operational and logical semantics for polling real-time systems, Technical Report CSI-R9813, Computer Science Institue Nijmegen, Faculty of Mathematics and Informatics, Catholic University of Nijmegen, April 1998, full paper of [13].
[15] H. Dierks, J. Tapken, Tool-supported hierarchical design of distributed real-time systems, in: Proc. 10th EuroMicro Workshop on Real Time Systems, IEEE Computer Society, June 1998, pp. 222-229.
[16] Hansen, M.R.; Chaochen, Zhou, Duration calculus: logical foundations, Formal aspects comput., 9, 283-330, (1997) · Zbl 0887.68101
[17] Harel, D., Statechartsa visual formalism for complex systems, Sci. comput. programming, 8, 231-274, (1987) · Zbl 0637.68010
[18] Harel, D., On visual formalisms, Comm. ACM, 31, 5, 514-530, (1988)
[19] IEC International Standard 1131-3, Programmable Controllers, Part 3, Programming Languages, 1993.
[20] K.-H. John, M. Tiegelkamp, SPS-Programmierung Mit IEC 1131-3, Springer, Berlin, 1995 (in German).
[21] Krieg-Brückner, B.; Peleska, J.; Olderog, E.-R.; Balzer, D.; Baer, A., Uniform – universal formal methods workbench, (), 357-378
[22] C. Lewerentz (Ed.), Formal Development of Reactive Systems: Case Study “Production Cell”, Lecture Notes in Computer Science, vol. 891, Springer, Berlin, 1995. · Zbl 0825.00053
[23] C. Lewerentz, T. Lindner (Eds.), Case Study “Production Cell”, Forschungszentrum Informatik, Karlsruhe, 1994.
[24] R.W. Lewis, Programming industrial control systems using IEC 1131-3, The Institution of Electrical Engineers, 1995.
[25] O. Maler, S. Yovine, Hardware timing verification using kronos, in: Proc. 7th Conf. on Computer-based Systems and Software Engineering, IEEE Press, New York, 1996.
[26] Müller-Olm, M., Modular compiler verification, lecture notes in computer science, vol. 1283, (1997), Springer Berlin
[27] A.P. Ravn, Design of embedded real-time computing systems, Technical Report 1995-170, Technical University of Denmark, 1995. · Zbl 0875.68006
[28] A.P. Ravn, H. Rischel (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science, vol. 1486, Lyngby, Denmark, Springer, Berlin, September 1998.
[29] Ravn, A.P.; Rischel, H.; Hansen, K.M., Specifying and verifying requirements of real-time systems, IEEE trans. software eng., 19, 41-55, (1993)
[30] M. Schenke, Development of correct real-time systems by refinement, Habilitation Thesis, University of Oldenburg, April 1997.
[31] J. Tapken, Interactive and compilative simulation of PLC-Automata, in: W. Hahn, A. Lehmann (Eds.), ESS’97, SCS, October 1997, pp. 552-556.
[32] J. Tapken, H. Dierks, MOBY/PLC - Graphical Development of PLC-Automata, in: A.P. Ravn, H. Rischel (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science, vol. 1486, Lyngby, Denmark, Springer, Berlin, September 1998, pp. 311-314.
[33] Chaochen, Zhou; Hoare, C.A.R.; Ravn, A.P., A calculus of durations, Inform. proc. lett., 40/5, 269-276, (1991) · Zbl 0743.68097
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.