Witness Report

Installation

To install witness-report, you have two options:

Install globally:

npm install -g witness-report

Install as a dependency in your project:

npm install witness-report

Usage

The easiest way to generate a report is via npx, with no installation required:

npx witness-report -i myInputPath -o myOutputPath

If you have installed witness-report globally, use it directly with:

witness-report -i myInputPath -o myOutputPath

To use witness-report in your code, install it as a dependency and use it like this:

const witness_report = require('witness-report');
//some code
witness_report.generate(inputPath, outputPath, override);
//some more code

Command Line Parameters

| Parameter | Alias | Required | Type | Description | |---------------|-----------|--------------|-----------|---------------------------------------------------------------------------------------------------------| | --input | -i | Required | string | Path to the input JSON or YAML file | | --output | -o | Optional | string | Desired path for the output HTML file.If not given, the output will be written to standard output. | | --override | -r | Optional | boolean | Set to true to override the output file if it exists | | --help | | Optional | boolean | Show help and ignore all other parameters |

Table: Command Line Parameters for Witness Report

Description

This tool was implemented as Bachelor's thesis. The written thesis provides extensive background information and documentation and will be linked here as soon as available. The following is a short introduction:

Witness Report is a lightweight HTML report tool designed for verification results. It takes a set of verification results along with their corresponding witnesses as input and generates a single HTML file as output, typically ranging from a few kilobytes to a small number of megabytes. This output file can be easily run in a browser and conveniently copied or shared. Unlike other tools, Witness Report does not require additional folders containing styling, JavaScript, or source files; everything is encoded within the HTML itself. The tool is designed to use minimal libraries and frameworks to be lightweight and for maintainability reasons. The UI adheres to the information hiding principle. Users can selectively view details from specific verification runs without being overwhelmed by excessive functionality and information.

The visualisation of verification results is based on the verification witness-format 2.0, which is explained in this paper. The tool expects either a JSON-file defining a set of results, which is the intended primary use, or a single witness file as input. An input JSON looks like this:

{
  "results": [
    {
      "analyzedFiles": [
        "../src/file1.c",
        "../src/file2.c"
      ],
      "entryFile": "../src/file1.c",
      "entryMethod": "method1",
      "result": "FALSE",
      "property": "CHECK(init(main()),LTL(G!call(reach_error()))",
      "resultWitness": "./file1_method1/output/witness.yml",
      "compileCommand": "myCommand"
    }
  ]
}

All paths must be relative to the JSON-file. This example is minimal. A "result" object can contain more than the specified attributes as the additional ones are simply ignored. But if it misses one of the attributes, an error is thrown.

Abstract

This thesis introduces Witness Report, a lightweight HTML-based visualization tool designed to address the complexities associated with formal software verification. As society's dependence on software continues to grow, so does the need for robust software quality assurance. Formal verification methods like model checking offer a strong approach for proving software correctness. Despite its potential, formal verification remains underutilized in industry due to the inherent complexity of the tools and the challenges developers face in interpreting verification results.

To address this problem, verification witnesses were introduced as a standardized format for documenting the results of verification runs, facilitating both human understanding and tool compatibility. One use case of these witnesses is result visualisation. However, there is currently only one major tool available for visualizing results, and it relies on an outdated witness format. Additionally, it requires a web server setup and always validates witnesses before visualizing them. While this is a valid approach, there remains a need for a lightweight tool that can visualize verification witnesses without any overhead.

Witness Report fills this gap by providing a lightweight, streamlined solution which allows developers and researchers to visualize verification witnesses easily without the need for extensive setup or additional infrastructure. By processing witness and source files into a single HTML report file, Witness Report enables interactive exploration of verification results, enhancing the debugging process and making formal verification more accessible. This thesis provides relevant background information about model checking and verification witnesses, and explains the design and implementation of Witness Report. It examines its architecture, use of technologies, user experience considerations, and explains how to use it. Additionally, the work discusses the implications and limitations of the tool, and outlines potential future applications and enhancements.

License

This project is licensed under the Apache License in Version 2.0 - see the LICENSE file for details.