[isabelle] New in the AFP: A Formal Development of a Polychronous Polytimed Coordination Language



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é

Attachment: signature.asc
Description: Message signed with OpenPGP



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.