HeKatE Verification and Analysis
HeaRT also provides a modularized verification framework, also known as HalVA (HeKatE Verification and Analysis).
Introduction
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.
Documentation
Using it
HalVA is integrated with HeaRT, so you need to download the engine.