Abstract
PLC-Automata are a class of real-time automata suitable to describe the behavior of polling real-time systems. PLC-Automata can be compiled to source code for PLCs, a hardware widely used in industry to control processes. Also, PLC-Automata have been equipped with a logical and operational semantics, using Duration Calculus (DC) and Timed Automata (TA), respectively.
The three main results of this paper are: (1) A simplified operational semantics. (2) A minor extension of the logical semantics, and a proof that this semantics is complete relative to our operational semantics. This means that if an observable satisfies all formulas of the DC semantics, then it can also be generated by the TA semantics. (3) A proof that the logical semantics is sound relative to our operational semantics. This means that each observable that is accepted by the TA semantics constitutes a model for all formulas of the DC semantics.
Supported by the German Ministery for Education and Research (BMBF), project UniForM, grant No. FKZ 01 IS 521 B3
Research supported by Netherlands Organization for Scientific Research (NWO) under contract SION 612-14-004
Supported by the HCM Network EXPRESS and the Deutsche Akademischer Austauschdienst
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
R. Alur, T.A. Henzinger, and E.D. Sontag, editors. Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and Wang Yi. UPPAAL: a tool suite for the automatic verification of real-time systems. In Alur et al. [2], pages 232–243.
C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool Kronos. In Alur et al. [2], pages 208–219.
H. Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata. In M. Bertran and T. Rus, editors, ARTS’97, volume 1231 of Lecture Notes in Computer Science, pages 111–125, Mallorca, Spain, May 1997. Springer-Verlag.
H. Dierks. Synthesising Controllers from Real-Time Specifications. In Tenth International Symposium on System Synthesis, pages 126–133. IEEE CS Press, September 1997.
H. Dierks and C. Dietz. Graphical Specification and Reasoning: Case Study “Generalized Railroad Crossing”. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, FME’97, volume 1313 of Lecture Notes in Computer Science, pages 20–39, Graz, Austria, September 1997. Springer-Verlag.
H. Dierks, A. Fehnker, A. Mader, and F. Vaandrager. Operational and logical semantics for polling real-time systems. CSI-R9813, University of Nijmegen, april 1998.
H. Dierks and J. Tapken. Tool-Supported Hierarchical Design of Distributed Real-Time Systems. In Proceedings of EuroMicro 98, 1998. to appear.
Z. Kohavi. Switching and Finite Automata Theory. McGraw-Hill, Inc., 1970.
B. Krieg-Brückner, J. Peleska, E.-R. Olderog, D. Balzer, and A. Baer. UniForM — Universal Formal Methods Workbench. In U. Grote and G. Wolf, editors, Statusseminar des BMBF Softwaretechnologie, pages 357–378. BMBF, Berlin, March 1996.
O. Maler and S. Yovine. Hardware Timing Verification using Kronos. In Proc. 7th Conf. on Computer-based Systems and Software Engineering. IEEE Press, 1996.
A.P. Ravn. Design of Embedded Real-Time Computing Systems. Technical Report 1995-170, Technical University of Denmark, 1995.
Zhou Chaochen. Duration Calculi: An overview. In D. BjØrner, M. Broy, and I.V. Pottosin, editors, Formal Methods in Programming and Their Application, volume 735 of Lecture Notes in Computer Science, pages 256–266. Springer-Verlag, 1993.
Zhou Chaochen, C.A.R. Hoare, and A.P. Ravn. A Calculus of Durations. Inform. Proc. Letters, 40/5:269–276, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dierks, H., Fehnker, A., Mader, A., Vaandrager, F. (1998). Operational and logical semantics for polling real-time systems. In: Ravn, A.P., Rischel, H. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1998. Lecture Notes in Computer Science, vol 1486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055334
Download citation
DOI: https://doi.org/10.1007/BFb0055334
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65003-4
Online ISBN: 978-3-540-49792-9
eBook Packages: Springer Book Archive