Operational and logical semantics for polling real-time systems

Henning Dierks, Ansgar Fehnker, Angelika H. Mader, Frits Vaandrager

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    12 Citations (Scopus)
    83 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publicationFormal Techniques in Real-Time and Fault-Tolerant Systems
    Subtitle of host publication5th International Symposium, FTRTFT’98 Lyngby, Denmark, September 14–18, 1998 Proceedings
    EditorsAnders P. Ravn, Hans Rischel
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages29-40
    Number of pages12
    ISBN (Electronic)978-3-540-49792-9
    ISBN (Print)978-3-540-65003-4
    DOIs
    Publication statusPublished - 1998
    Event5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT 1998 - Lyngby, Denmark
    Duration: 14 Sep 199818 Sep 1998
    Conference number: 5

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume1486
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT 1998
    Abbreviated titleFTRTFT
    CountryDenmark
    CityLyngby
    Period14/09/9818/09/98

    Fingerprint

    Dive into the research topics of 'Operational and logical semantics for polling real-time systems'. Together they form a unique fingerprint.

    Cite this