erwanm974 / coq_hibou_label_equivalent_terms

Formal proof with the Coq theorem prover that elements of some equivalence classes defined over a formal language of interactions describing the behavior of distributed systems have the same semantics.

Coq proof for the definition of equivalence classes that preserve the semantics on interaction terms as used by HIBOU LABEL

This repository hosts a proof written in the Gallina language. We use the Coq automated theorem prover to (1) define equivalence classes on the set of interaction terms for a formal language of "interactions" and (2) prove that all elements of those equivalence classes have the same semantics w.r.t. a denotational-style semantics for this interaction language.

"Interactions" model the behavior of distributed systems and can be considered to be a formalisation of UML Sequence Diagrams.

A web page (generated with coqdoc) presenting the proof can be accessed here.

A prototype tool, which makes use of some of those transformations to simplify interaction terms as they are being used and rewritten through an operational-style semantics to implements various model-based testing features is available on this repository.