Выводы по главе 4
1. В рамках работы по государственному контракту [65 -69]была проведена апробация инструментального средства Converterна модели банкомата, содержащего два вложенных автомата с 13 и пятью состояниями.
Были формально верифицированы как истинные свойства банкомата, так и построены контрпримеры для ложных свойств.2. Converterи Staterиспользуются в учебном процессе. С 2012 года автором на кафедре «Компьютерные технологии» ведётся курс по верификации программного обеспечения. В рамках его студенты провели верификацию автоматных программ, выложенных на сайте http://is.ifmo.ru. В одной из программ была найдена ошибка, несмотря на то, что она многократно проверялась до этого.
3. Инструментальное средство Staterбыло использовано в ООО «СТЦ» для верификации части программы AntsysEditor, позволяющей обрабатывать XML-файлы, которые содержат информацию о структуре антенн. Внедрение подтверждается актом о внедрении. Построенная при помощи Staterмодель и вывод Spinприведены в Приложении А.
4. Инструментальное средство Starterбыло использовано для верификации логики в игре «Turtleball HD», что также подтверждается актом о внедрении. Построенная при помощи Staterмодель и вывод Spin приведены в Приложении Б.