Back End

All backEnd code is located inside src/backEnd directory.

src/backend/common

src/backEnd/common/Kind2Utils.m

Kind2Utils.verify

Currently there are 2 implementations for verification: src/backEnd/cocoSpecVerify and src/backEnd/lustreVerify.

src/backEnd/cocoSpecVerify

This implementation supports contracts and compositional analysis. Currently it only supports Kind2 model checker. This module consists of the following functions:

• src/backEnd/cocoSpecVerify/cocoSpecVerify.m: This function is invoked by cocosim_window when the translation from IR to Lustre is finished. Then it invokes the chosen model checker to verify the generated code. Since currently only Kind2 supports contracts, there is only one corresponding function cocoSpecKind2 that can be called.
• src/backEnd/cocoSpecVerify/utils/cocoSpecKind2: this is the main function in src/backEnd/cocoSpecVerify. It receives a path to the preprocessed model and a path to the mapping file generated by the translator. The function does the following:
  • Calls Kind2Utils.verify to verify the Lustre file.
  • Reads the xml file generated by Kind2.
  • Reads the json mapping file that maps blocks to the names in the Lustre file.
  • Extracts properties (assume, guarantee and ensure) from the contents of the json file into a map
  • Reads corresponding properties from the xml file and group them using the tags AnalysisStart and AnalysisStop. There are special cases to be handled:
    • _one_mode_active property is not available in the mapping file. Therefore, it is mapped to the validator block of its contract
    • If the property is falsifiable (CEX), the counter example is read from the XML file.
  • Saves the result in a model variable called verificationResults.
  • Calls displayVerificationResults to display the verification results.

src/backEnd/cocoSpecVerify/utils

displayVerificationResults.m

src/backEnd/lustreVerify

[to be completed]