On specifying real-time systems in a causality-based setting

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

    28 Citations (Scopus)
    3 Downloads (Pure)

    Abstract

    Event structures are a prominent noninterleaving model for concurrency. Real-time event structures associate a set of time instants to events, modelling absolute time constraints, and to causal dependencies, modelling relative delays between causally dependent events. We introduce this novel temporal model and show how it can be used to provide a denotational semantics to a real-time variant of a process algebra akin to LOTOS. This formalism includes a timed-action prefix which constrains the occurrence time of actions, a timeout and watchdog (i.e., timed interrupt) operator. An event-based operational semantics for this formalism is presented that is shown to be consistent with the denotational semantics. As an example we use an infinite buffer with time constraints on the message latency and the rates of accepting and producing data.
    Original languageEnglish
    Title of host publicationFormal Techniques in Real-Time and Fault-Tolerant Systems
    Subtitle of host publication4th International Symposium Uppsala, Sweden, September 9–13, 1996, Proceedings
    EditorsBengt Jonsson, Joachim Parrow
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages385-405
    Number of pages21
    ISBN (Electronic)978-3-540-70653-3
    ISBN (Print)978-3-540-61648-1
    DOIs
    Publication statusPublished - 1996
    Event4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996 - Uppsala, Sweden
    Duration: 9 Sep 199613 Sep 1996
    Conference number: 4

    Publication series

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

    Conference

    Conference4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996
    Abbreviated titleFTRTFT
    CountrySweden
    CityUppsala
    Period9/09/9613/09/96

    Fingerprint

    semantics
    formalism
    messages
    algebra
    buffers
    occurrences
    operators

    Keywords

    • FMT-PA: PROCESS ALGEBRAS
    • FMT-NIM: NON-INTERLEAVING MODELS
    • Event structure
    • Operational semantics
    • Parallel composition
    • Process algebra
    • Denotational semantics

    Cite this

    Katoen, J-P., Langerak, R., Latella, D., & Brinksma, E. (1996). On specifying real-time systems in a causality-based setting. In B. Jonsson, & J. Parrow (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems: 4th International Symposium Uppsala, Sweden, September 9–13, 1996, Proceedings (pp. 385-405). (Lecture Notes in Computer Science; Vol. 1135). Berlin, Heidelberg: Springer. https://doi.org/10.1007/3-540-61648-9_52
    Katoen, Joost-Pieter ; Langerak, Rom ; Latella, Diego ; Brinksma, Ed. / On specifying real-time systems in a causality-based setting. Formal Techniques in Real-Time and Fault-Tolerant Systems: 4th International Symposium Uppsala, Sweden, September 9–13, 1996, Proceedings. editor / Bengt Jonsson ; Joachim Parrow. Berlin, Heidelberg : Springer, 1996. pp. 385-405 (Lecture Notes in Computer Science).
    @inproceedings{1aea86110ca54712ab9821064011f783,
    title = "On specifying real-time systems in a causality-based setting",
    abstract = "Event structures are a prominent noninterleaving model for concurrency. Real-time event structures associate a set of time instants to events, modelling absolute time constraints, and to causal dependencies, modelling relative delays between causally dependent events. We introduce this novel temporal model and show how it can be used to provide a denotational semantics to a real-time variant of a process algebra akin to LOTOS. This formalism includes a timed-action prefix which constrains the occurrence time of actions, a timeout and watchdog (i.e., timed interrupt) operator. An event-based operational semantics for this formalism is presented that is shown to be consistent with the denotational semantics. As an example we use an infinite buffer with time constraints on the message latency and the rates of accepting and producing data.",
    keywords = "FMT-PA: PROCESS ALGEBRAS, FMT-NIM: NON-INTERLEAVING MODELS, Event structure, Operational semantics, Parallel composition, Process algebra, Denotational semantics",
    author = "Joost-Pieter Katoen and Rom Langerak and Diego Latella and Ed Brinksma",
    year = "1996",
    doi = "10.1007/3-540-61648-9_52",
    language = "English",
    isbn = "978-3-540-61648-1",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "385--405",
    editor = "Bengt Jonsson and Joachim Parrow",
    booktitle = "Formal Techniques in Real-Time and Fault-Tolerant Systems",

    }

    Katoen, J-P, Langerak, R, Latella, D & Brinksma, E 1996, On specifying real-time systems in a causality-based setting. in B Jonsson & J Parrow (eds), Formal Techniques in Real-Time and Fault-Tolerant Systems: 4th International Symposium Uppsala, Sweden, September 9–13, 1996, Proceedings. Lecture Notes in Computer Science, vol. 1135, Springer, Berlin, Heidelberg, pp. 385-405, 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996, Uppsala, Sweden, 9/09/96. https://doi.org/10.1007/3-540-61648-9_52

    On specifying real-time systems in a causality-based setting. / Katoen, Joost-Pieter; Langerak, Rom; Latella, Diego; Brinksma, Ed.

    Formal Techniques in Real-Time and Fault-Tolerant Systems: 4th International Symposium Uppsala, Sweden, September 9–13, 1996, Proceedings. ed. / Bengt Jonsson; Joachim Parrow. Berlin, Heidelberg : Springer, 1996. p. 385-405 (Lecture Notes in Computer Science; Vol. 1135).

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

    TY - GEN

    T1 - On specifying real-time systems in a causality-based setting

    AU - Katoen, Joost-Pieter

    AU - Langerak, Rom

    AU - Latella, Diego

    AU - Brinksma, Ed

    PY - 1996

    Y1 - 1996

    N2 - Event structures are a prominent noninterleaving model for concurrency. Real-time event structures associate a set of time instants to events, modelling absolute time constraints, and to causal dependencies, modelling relative delays between causally dependent events. We introduce this novel temporal model and show how it can be used to provide a denotational semantics to a real-time variant of a process algebra akin to LOTOS. This formalism includes a timed-action prefix which constrains the occurrence time of actions, a timeout and watchdog (i.e., timed interrupt) operator. An event-based operational semantics for this formalism is presented that is shown to be consistent with the denotational semantics. As an example we use an infinite buffer with time constraints on the message latency and the rates of accepting and producing data.

    AB - Event structures are a prominent noninterleaving model for concurrency. Real-time event structures associate a set of time instants to events, modelling absolute time constraints, and to causal dependencies, modelling relative delays between causally dependent events. We introduce this novel temporal model and show how it can be used to provide a denotational semantics to a real-time variant of a process algebra akin to LOTOS. This formalism includes a timed-action prefix which constrains the occurrence time of actions, a timeout and watchdog (i.e., timed interrupt) operator. An event-based operational semantics for this formalism is presented that is shown to be consistent with the denotational semantics. As an example we use an infinite buffer with time constraints on the message latency and the rates of accepting and producing data.

    KW - FMT-PA: PROCESS ALGEBRAS

    KW - FMT-NIM: NON-INTERLEAVING MODELS

    KW - Event structure

    KW - Operational semantics

    KW - Parallel composition

    KW - Process algebra

    KW - Denotational semantics

    U2 - 10.1007/3-540-61648-9_52

    DO - 10.1007/3-540-61648-9_52

    M3 - Conference contribution

    SN - 978-3-540-61648-1

    T3 - Lecture Notes in Computer Science

    SP - 385

    EP - 405

    BT - Formal Techniques in Real-Time and Fault-Tolerant Systems

    A2 - Jonsson, Bengt

    A2 - Parrow, Joachim

    PB - Springer

    CY - Berlin, Heidelberg

    ER -

    Katoen J-P, Langerak R, Latella D, Brinksma E. On specifying real-time systems in a causality-based setting. In Jonsson B, Parrow J, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems: 4th International Symposium Uppsala, Sweden, September 9–13, 1996, Proceedings. Berlin, Heidelberg: Springer. 1996. p. 385-405. (Lecture Notes in Computer Science). https://doi.org/10.1007/3-540-61648-9_52