Name
Abstract | ||
|---|---|---|
In this paper, we study the semantics of a specification language for the coordination of concurrent systems, which supports time at different levels: various time domains, polychrony, and mixed metric/logical time constraints. The language itself is defined by a denotational semantics. In order to be able to construct the possible timelines for verification purposes, we also define a symbolic operational semantics, which is the reference for an efficient implementation of a tool for runtime-testing of heterogeneous systems. This study presents a novel way to link these two semantics by taking advantage of a coinductive unfolding principle of these timelines. Furthermore, these semantics and their equivalence have been formalized in the Isabelle/HOL proof assistant, together with proofs for soundness, completeness and progress. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/978-3-030-57628-8_2 | FORMATS |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hai Nguyen Van | 1 | 0 | 0.68 |
| Thibaut Balabonski | 2 | 20 | 6.56 |
| Frédéric Boulanger | 3 | 105 | 17.17 |
| Chantal Keller | 4 | 0 | 0.34 |
| Benoît Valiron | 5 | 228 | 21.00 |
| Burkhart Wolff | 6 | 1 | 1.02 |