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

Joost-Pieter Katoen; Rom Langerak; Diego Latella; Ed Brinksma

doi:10.1007/3-540-61648-9_52

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

Joost-Pieter Katoen, Rom Langerak, Diego Latella, Ed Brinksma

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

28 Citations (Scopus)

196 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 language	English
Title of host publication	Formal Techniques in Real-Time and Fault-Tolerant Systems
Subtitle of host publication	4th International Symposium Uppsala, Sweden, September 9–13, 1996, Proceedings
Editors	Bengt Jonsson, Joachim Parrow
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	385-405
Number of pages	21
ISBN (Electronic)	978-3-540-70653-3
ISBN (Print)	978-3-540-61648-1
DOIs	https://doi.org/10.1007/3-540-61648-9_52
Publication status	Published - 1996
Event	4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996 - Uppsala, Sweden Duration: 9 Sept 1996 → 13 Sept 1996 Conference number: 4

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1135
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996
Abbreviated title	FTRTFT
Country/Territory	Sweden
City	Uppsala
Period	9/09/96 → 13/09/96

Keywords

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

Access to Document

10.1007/3-540-61648-9_52

Katoen1996onSubmitted version, 371 KB
Katoen1996onFinal published version, 1.08 MB

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). Springer. https://doi.org/10.1007/3-540-61648-9_52

Katoen, Joost-Pieter ; Langerak, Rom ; Latella, Diego et al. / 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",

address = "Germany",

note = "4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996, FTRTFT ; Conference date: 09-09-1996 Through 13-09-1996",

}

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 et al.
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 proceeding › Conference contribution › Academic › peer-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

N1 - Conference code: 4

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

T2 - 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996

Y2 - 9 September 1996 through 13 September 1996

ER -

Katoen JP , 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). doi: 10.1007/3-540-61648-9_52

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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this