13 / 16
Разработка и исследование синтетического метода верификации программы…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4
61
Окончание табл. 4
Заданные свойства ПО
Алгоритмы
Синтетический
метод
LLBMC
Встроенные проверки
кода
+
–
+
Пользовательские про-
верки (assert и assume)
+
+
+
Статический анализ
+
+
+
Динамический анализ
–
–
+
Проверка моделей
–
–
+
Выводы.
Приведен синтетический метод верификации ПО. Метод позво-
ляет решить проблему комбинаторного взрыва, охватывает все заданные свой-
ства проверяемой программы, не требует построения наиболее полной сложной
модели программы. В результате работы был получен алгоритм работы метода
верификации и его реализация на языке SMT–LIB. Предложенный метод и ал-
горитмы являются новыми. Автоматически осуществляется компиляция про-
граммы в ее внутреннее представление, построение инварианта программы по
ее внутреннему представлению и построение контрпримера к проверяемому
свойству ПО. Построение контрпримеров допускает участие экспертов.
ЛИТЕРАТУРА
1.
Бурякова Н.А., Чернов А.В
. Классификация частично формализованных и формаль-
ных моделей и методов верификации программного обеспечения // Электрон. науч.
жур. «Инженерный вестник Дона». 2010. Т. 14. № 4. URL:
http://www.ivdon.ru/ru/magazine/archive/n4y2010/259
2.
Вельдер С.Э., Шалыто А.А.
Верификация простых автоматных программ на основе
метода ModelChecking // Материалы XV Междунар. науч.-методич. конф. «Высокие ин-
теллектуальные технологии и инновации в образовании и науке». 2008. C. 286.
3.
Holzmann G., Smith M
. Software model checking: Extracting verification models from
source code // Formal methods for protocol engineering and distributed systems. Kluwer
Academic Publ., 1999. P. 481–497.
4.
Clarke E., Kroening D., Lerda F
. A tool for checking ANSI-C programs // Tools and algo-
rithms for the construction and analysis of systems (TACAS 2004) / Ed. by K. Jensen,
A. Podelski. Vol. 2988 of Lecture Notes in Computer Science. Springer, 2004. P. 168–176.
5.
Counterexample-guided
abstraction refinement / E. Clarke, O. Grumberg, S. Jha et al. //
Computer Aided Verification. 2000. P. 154–169.
6.
Software
verification with blast / T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre // 10th
SPIN Workshop on Model Checking Software (SPIN). LNCS 2648. Springer-Verlag, 2003.
P. 235–239.
7.
Cousot P
. Abstract interpretation. ACM Computing Surveys (CSUR) // ACM. New York.
1996. Vol. 28. Iss. 2. P. 324–328.
8.
Глухих М.И., Ицыксон В.М., Цесько В.А
. Использование зависимостей для повыше-
ния точности статического анализа программ // Модел. и анализ информ. систем. 2011.
№ 4. C. 72–73.