VERIFICATION OF AUTOMATA-BASED PROGRAMS WITH SMV TOOL

E. . Kurbatsky


Read the full article 

Abstract

We consider the method of verification of automata-based programs using Model Checking method. To verify the model the tool SMV is used. In the proposed approach, transition system is not built in explicit form. This allows the program to verify systems with large number of states.


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

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