Computing, Telecommunication and Control Информатика, телекоммуникации и управление 2687-0517 22 Verification of requirements for reactive systems Статический анализ требований реактивных систем Ivanov Аleksandr al.s.ivanov@gmail.com Kotlyarov Vsevolod vpk@spbstu.ru Letichevsky Aleksandr let@cyfra.net Peter the Great St.Petersburg Polytechnic University 10 08 2012 4 152 109 114

The article features an approach for verification of requirements for reactive systems represented in the basic model notation. An examples of use are reviewed. The benefits and restrictions of this technology are revealed and discussed.

 formal verification formal notation Hoare logic requirement management