Home     |     Publications/Talks     |     Formal proofs     |   Thesis

     The objective of this formalisation is to provide a framework for reasoning on distributed component models, component configuration, components at runtime, and futures. Participants to this formalisation were: Muhammad Uzair Khan, Florian Kammüller, and Ludovic Henrio .

     We provide a formal model for distributed components communicating asynchronously using futures. The communication model is based on a request-reply paradigm, where requests are enqueued at target component and invoker receives a future, representing the result.  When the results are available, they are sent to the relevant components using a future update strategy. Future update strategies are somewhat neglected in the literature. We believe that even though future update strategies need not be included for studying properties of a language, they are still important for reasoning on the implementation of this language. Consequently, our semantics include formalisation of a future update strategy.  All of our work, the component model specification, its semantics, and proofs of properties, has been mechanised in isabelle/HOL. These mechanised proofs ensure the correctness of the implementation of future updates in ProActive/GCM.