VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH UNIMOD.VERIFIER TOOL

V. . Gurov, B. . Jaminov


Read the full article 

Abstract

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.


Keywords: program verification, model checking, automata-based programming
Copyright 2001-2017 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика