Например, Бобцов

VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH UNIMOD.VERIFIER TOOL

Аннотация:

This article describes the verifier of automata-based programs created with the tool to support automata-based programming UniMod. Verifier works by integrating tool UniMod and verifier Bogor. Using developed verifier there is no need to convert automata-based program to the input language of the verifier. Requirements for the program are written in the language of temporal logic LTL.

Ключевые слова:

Статьи в номере