Detail aplikovaného výsledku

Překladač modelu FAST pro ARMC

SMRČKA, A.

Originální název

Překladač modelu FAST pro ARMC

Anglický název

FAST to ARMC Translator

Druh

Software

Abstrakt

Program překládá modely pro nástroje FAST nebo FASTer, aby byly použitelné pro model checker ARMC. Cíl projektu je využít robustnost nástroje ARMC pro řadu modelů napsaných pro nástroj FAST. Překladač kompletně rozumí definici modelu v jazyku FAST a některé hlavní části popisu strategie verifikace modelu. Překladač může být jednoduše přepsán tak, aby podporoval jiné výstupní jazyky. Uživateli je tak umožněno pomocí různých verifikačních nástrojů ověřit řadu modelů specifikovaných jazykem FAST.

Abstrakt aglicky

The program translates a model for FAST or for FASTer tool to ARMC model checker. The goal of the project is to achieve better experiment results of many of FAST models due to great effectiveness of ARMC (almost 7x faster then FASTer on several models). The translator completely understands a FAST/FASTer model specification and the main part of strategy description. The translator can be simply rewriten to support different output languages so the user is then able to write the model in one language (FAST) and verify it in different tools.

Klíčová slova

VHDL, counter automata, translator, model, formal verification

Klíčová slova anglicky

VHDL, counter automata, translator, model, formal verification

Umístění

http://fast2armc.sourceforge.net/

Možnosti využití

výsledek využívá pouze poskytovatel

Licenční poplatek

K využití výsledku jiným subjektem je vždy nutné nabytí licence

www

http://fast2armc.sourceforge.net/

Dokumenty

fast2armc-1.2.1.tar