HeKatE Verification and Analysis

HeaRT also provides a modularized verification framework, also known as HalVA (HeKatE Verification and Analysis).

The framework uses the logical formalization of the XTT2 model usling the ALSVfd logic.

It is based of previous work of Prof. Antoni Ligęza, and Dr. Grzegorz J. Nalepa.

Current implementation has been carried out by Agata Ligęza, MSc., with support of Szymon Bobek, MSc, and testing by Krzysztof Kaczor, MSc.

Verification and analysis module implements:

• simple debugging mechanism that allows tracking system's work,
• export to LaTeX mechanism which provides functionality of exporting entire model to TEX file,
• logical verification of models (several plugins are available, including completeness, determinism and redundancy checks), and
• syntactic analysis of HMR files using a DCG grammar of HMR.

The verification plugins can be run from the interpreter or indirectly from HQEd using the communication protocol.

See the general HeaRT Architecture and the Verifying Models howto.

HalVA is integrated with HeaRT, so you need to download the engine.