This shows you the differences between two versions of the page.

Link to this comparison view

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.
hekate/halva.txt · Last modified: 2019/06/27 15:49 (external edit)
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0