This shows you the differences between two versions of the page.
|
hekate:halva [2019/06/27 15:49] |
hekate:halva [2019/06/27 15:49] (current) |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| + | ====== 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 ===== | ||
| + | See the general [[hekate:heart_overview#HeaRT Architecture]] and | ||
| + | the [[hekate:heart_howto#Verifying Models]] howto. | ||
| + | |||
| + | ===== Using it ===== | ||
| + | HalVA is integrated with [[HeaRT]], so you need to [[hekate:heart#releases|download]] the engine. | ||
