Operational and logical semantics for polling real-time systems


Share/Save/Bookmark

Dierks, Henning and Fehnker, Ansgar and Mader, Angelika and Vaandrager, Frits (1998) Operational and logical semantics for polling real-time systems. In: 5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT, September 14–18, 1998, Lyngby, Denmark.

[img]
Preview
PDF
222Kb
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.
Item Type:Conference or Workshop Item
Copyright:© 1998 Springer-Verlag
Link to this item:http://purl.utwente.nl/publications/56216
Official URL:http://dx.doi.org/10.1007/BFb0055334
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page