Skip to content

Home

Jump to bottom
Alberto Tacchella edited this page Dec 7, 2018 · 16 revisions

This wiki contains the implementation notes for the BT translation tools.

Roadmap

  • Write a Coq module defining the BT data type, some helper functions, and (perhaps) prove some useful lemmas about them.

    STATUS: done; two implementations available (binary branching/arbitrary branching), the second one is generally to be preferred.

  • (deliverable 4.1) Realize the abstract operational semantics of BTs in Coq.

    STATUS: done via a shallow embedding of the operational semantics as a Gallina program.

  • (deliverable 5.1) Implement the semantics of NuSmv HFSM execution in Coq and prove the equivalence with the cerfified interpreter.

    STATUS: done; an informal equivalence proof can be found in the D5.1 report.

  • (deliverable 5.2) Write a tool to extract from a BT + annotations a formal specification which can be feeded directly into the NuSMV and OCRA tools.

    STATUS: done; deep embedding of (micro-)SMV language into Coq completed, translation tool & automatic generation of OCRA input file working as sketched in the August, 1st meeting.

Clone this wiki locally