Email Gateway (Aug 22 2022 at 20:11): Email Gateway (Aug 22 2022 at 20:11):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
A Formal Development of a Polychronous Polytimed Coordination Language
by Hai Nguyen Van, Frédéric Boulanger and Burkhart Wolff
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.
See https://www.isa-afp.org/entries/TESL_Language.html for more details.
Enjoy,
René
signature.asc
Last updated: Apr 26 2024 at 20:16 UTC