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

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

28 Citations (Scopus)
1 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