Skip to content

Back End

Jump to bottom
mudathirmahgoub edited this page Jun 9, 2018 · 10 revisions

All backEnd code is located inside src/backEnd directory.

src/backend/common

src/backEnd/common/Kind2Utils.m

This class contains common functions that are related to Kind2 model checker.

Kind2Utils.verify

This function receives a path to Lustre file and arguments for Kind2. Then it invokes kind2 binary based on the user preferences (local, docker, or kind2 web service). Finally it returns the raw XML output of Kind2.

Kind2Utils.simulate

This function receives a path to Lustre file and a path to the input file for the interpreter. Then it invokes kind2 binary based on the user preferences (local, docker, or kind2 web service). Finally it returns raw the XML output of Kind2.

Kind2Utils.parseSimulation

Kind2Utils.simulate returns the raw XML output of kind2. Kind2Utils.parseSimulation parses the XML into a MATLAB structure.

Verification

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

This function receives as arguments the verification results and a map for compositional analysis which stores the current selected analyses. It does the following:

  • Resets the colors and the masks of the blocks in the model by calling initializeVerificationVisualization.
  • Changes the background colors of property blocks (assume, guarantee, ensure and validator) based on the property answer. The colors meanings are explained in property colors
  • Adds the following mask actions (buttons) to blocks that with falsified properties:
    • Display counter example as signals which calls the function displayCexSignals.
    • Display counter example as tables which calls the function displayCexTables.
    • Display counter example as HTML tables which calls the function displayCexHtmlTables.
    • Generate an outer model for the counter example which calls the function generateModelWithSignalBuilders with level = 2.
    • Generate an inner model for the counter example which calls the function generateModelWithSignalBuilders with level = 1.
  • Changes the colors of subsystem blocks and contract blocks based on color of underlying properties. The colors meanings are explained in subsystem colors.

displayCexSignals.m

This function receives 2 indices: the first for verification analysis and the second for the property in that analysis. The function displays the property counter example using signals as follows:

  • Reads the property structures and the counter example stored in the model workspace.
  • Determines the number time steps from the counter example. Since signals use intervals, the function increases the number of steps by one and repeating the last value of each stream.
  • Chooses random colors for each signal.
  • Display the signals and their labels.

displayCexTables.m

This function receives 2 indices: the first for verification analysis and the second for the property in that analysis. The function displays the property counter example using tables as follows:

  • Reads the property structures and the counter example stored in the model workspace.
  • Flattens all nodes in the counter example which are stored recursively.
  • Displays each node as a table starting from the last node down to the first node as follows:
    • Sets column names to be the time steps of the counter example.
    • Sets the row names to be the name of stream + the class(input, local, output) of the stream.
    • Sets the table name to be the origin path of the property.
    • Sets the data of the table to be the streams data.
  • Adds a sliders to scroll up and down.

displayCexHtmlTables.m

This function receives 2 indices: the first for verification analysis and the second for the property in that analysis. The function displays the property counter example using HTML tables as follows:

  • Reads the property structures and the counter example stored in the model workspace.
  • Flattens all nodes in the counter example which are stored recursively.
  • Builds a Matlab struct named property from the counter example.
    • Sets column names to be the time steps of the counter example.
    • Sets the row names to be the name of stream + the class(input, local, output) of the stream.
    • Sets the table name to be the origin path of the property.
    • Sets the data of the table to be the streams data.
  • Reads the content of the file cexTemplate.html.
  • Replaces [(property)] with the json encoding of property, and saves the results into a temporary files.
  • Adds the requierd css and js files to the temporary folder.
  • Opens the html file using MATLAB Web browser.

generateModelWithSignalBuilders.m

This function receives 3 arguments: an index for verification analysis and another index for the property in that analysis. The third parameter level which determines the level of the diagram to be generated. level = 1 means the diagram one level above the current property, and levels = 2 means the diagram 2 levels above the current property. This function replaces the inports of the generated model with the values from the counter example as follows:

  • Reads the property structures and the counter example stored in the model workspace.
  • Reads the model name and shortens its length to 63 character if it is larger than that (MATLAB restriction on model names).
  • Sets the configurations of the simulation to be discrete and fixed step with one.
  • Generates a new model and opens it
  • Copy the diagram from the specified level.
  • Adds a signal builder to each inport.
  • Disconnects inports from other blocks.
  • Removes inport blocks.
  • Adds conversion blocks for signal builders to match the type in the counter example because signal builders always generate signals of type double.
  • Connects the signal builders with blocks which were connected to the removed inports.

src/backEnd/lustreVerify

[to be completed]

Clone this wiki locally