|
A
Formal
Development
of
a
Polychronous
Polytimed
Coordination
Language
Title: |
A Formal Development of a Polychronous Polytimed Coordination Language |
Authors:
|
Hai Nguyen Van (hai /dot/ nguyenvan /dot/ phie /at/ gmail /dot/ com),
Frédéric Boulanger (frederic /dot/ boulanger /at/ centralesupelec /dot/ fr) and
Burkhart Wolff
|
Submission date: |
2019-07-30 |
Abstract: |
The design of complex systems involves different formalisms for
modeling their different parts or aspects. The global model of a
system may therefore consist of a coordination of concurrent
sub-models that use different paradigms. We develop here a theory for
a language used to specify the timed coordination of such
heterogeneous subsystems by addressing the following issues:
- the
behavior of the sub-systems is observed only at a series of discrete
instants,
- events may occur in different sub-systems at unrelated
times, leading to polychronous systems, which do not necessarily have
a common base clock,
- coordination between subsystems involves
causality, so the occurrence of an event may enforce the occurrence of
other events, possibly after a certain duration has elapsed or an
event has occurred a given number of times,
- the domain of time
(discrete, rational, continuous...) may be different in the
subsystems, leading to polytimed systems,
- the time frames of
different sub-systems may be related (for instance, time in a GPS
satellite and in a GPS receiver on Earth are related although they are
not the same).
Firstly, a denotational semantics of the language is
defined. Then, in order to be able to incrementally check the behavior
of systems, an operational semantics is given, with proofs of
progress, soundness and completeness with regard to the denotational
semantics. These proofs are made according to a setup that can scale
up when new operators are added to the language. In order for
specifications to be composed in a clean way, the language should be
invariant by stuttering (i.e., adding observation instants at which
nothing happens). The proof of this invariance is also given. |
BibTeX: |
@article{TESL_Language-AFP,
author = {Hai Nguyen Van and Frédéric Boulanger and Burkhart Wolff},
title = {A Formal Development of a Polychronous Polytimed Coordination Language},
journal = {Archive of Formal Proofs},
month = jul,
year = 2019,
note = {\url{http://isa-afp.org/entries/TESL_Language.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|