Статья

Название статьи РАЗРАБОТКА ALL-SAT-РЕШАТЕЛЯ ДЛЯ ПОИСКА ВЕРИФИКАЦИОННЫХ НАБОРОВ В ТЕСТИРОВАНИИ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ
Автор И. А. Ляпунова, М. Н. Левченко, В. В. Гривцов
Рубрика РАЗДЕЛ II. МОДЕЛИРОВАНИЕ И АЛГОРИТМЫ ОБРАБОТКИ ИНФОРМАЦИИ
Месяц, год 07, 2018
Индекс УДК 004.04
DOI 10.23683/2311-3103-2018-7-133-143
Аннотация Существует множество методов обнаружения ошибок и контроля качества программ, совокупность которых называется верификацией программного обеспечения. На сегодняшний день активно развиваются системы, предполагающие автоматическое доказательство соответствия программного обеспечения так называемой спецификации, т.е. предъявляемым к нему требованиям. Тем не менее, в большинстве проектов в основе процесса верификации до сих пор стоит именно тестирование. Зачастую этим занимаются люди, задачей которых является разработка тестов для поиска ошибок, допущенных в коде программистами. Упрощённо тесты представляют собой набор «входных» параметров, подающихся на вход в программу, а по завершении ее работы «выходные» параметры сравниваются с «ожидаемыми» по логике, описанной в спецификации. Тестирование является наиболее распространенным методом выявления ошибок в работе программного обеспечения и уже в 60-х годах использовалось для проверки программ, применяющихся в научных исследованиях, в авиакосмической отрасли, энергетике, медицине и прочих сложных системах. Процесс тестирования подобных продуктов проводился строго формализованно и в основе этого процесса стояла разработка тестовых процедур, которая проводилась на низком уровне автоматизации, и за более чем 50 лет развитие в этой области было несущественным. В начале 70-х годов тестирование определялось как «процесс, направленный на демонстрацию корректности работы программы», но вскоре стало ясно, что оно не способно выявить все критические ошибки проверяемого софта, но актуальности применения не потеряло. Такой вывод был подтвержден рядом происшествий, из-за которых крупные компании и государственные учреждения понесли большие финансовые потери. Ярким примером может служить крушение космического аппарата Mariner-1, произошедшее 22 июля 1962 года из-за ошибки в программе бортового компьютера. Таким образом, тестирование можно определить, как многократное выполнение программы с намерением найти в ней ошибки, но это в свою очередь не доказывает её корректность. В настоящей работе рассматривается применение SAT-решателей для решения проблемы поиска верификационных наборов для тестирования программного обеспечения и разработка модификация ALL-SAT-решателя.

Скачать в PDF

Ключевые слова Тестовые наборы; автоматическая генерация; решатель, булевы ограничения.
Библиографический список 1. Gu J., Purdom P.W., Franco J., Wah B.W. Algorithms for satisfiability (SAT) problem:
A survey. DIMACS Volume Series on Discrete Mathematics and Theoretical Computer Science: The Satisfiability (SAT) Problem. Vol. 35. American Mathematical Society, Providence, RI. – P. 19-151.
2. Een N., Sorensson N. An Extensible SAT-solver // in SAT. – 2003. – P. 502-508.
3. Levin L.A. Universal sequential search problems // Problems of Information Transmission.
– 1973. – No. 9:3. – P. 265-266.
4. Богданов Д.С. Автоматизированная генерация верификационных наборов тестовых процедур // ВКР. Южный Федеральный Университет, 2017.
5. Богданов Д.С., Ляпунова И.А., Тетруашвили Е.В. Задача разработки SAT-решателя для поиска верификационных наборов в тестирования программного обеспечения // Инженерный вестник Дона. – 2017. – № 4. – С. 77.
6. Кажаров Х.А., Ляпунова И.А., Чистяков А.Е. Программная реализация численного решения обратной задачи транспорта веществ // Инженерный вестник Дона. – 2015. – № 4 (38). – URL: ivdon.ru/ru/magazine/archive/n4y2015/3437.
7. Дегтярева Е.Е., Проценко Е.А., Чистяков А.Е. Программная реализация трехмерной математической модели транспорта взвеси в мелководных акваториях // Инженерный вестник Дона. – 2012. – № 4-2 (23). – URL: ivdon.ru/ru/magazine/archive/n4p2y2012/1283.
8. Семёнов А.А. О преобразованиях Цейтина в логических уравнениях // Теоретические основы прикладной дискретной математики. – 2009. – C. 28-50.
9. Mitchell D. Linear Time: Unit Propagation and Horn-SAT // Notes on Satisfiability-Based Problem Solving. – 2015. – P. 1-5.
10. Цейтин Г.С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ АН СССР. – 1968. – Т. 8. – C. 234-259.
11. Semenov A., Zaikin O. Using Monte Carlo method for searching partitionings of hard variants of Boolean satisfiability problem. In: Malyshkin, V. (ed.) // Parallel Computing Technologies - 13th International Conference, PaCT 2015, Petrozavodsk, Russia, August 31 - September 4, 2015: Proceedings. Lecture Notes in Computer Science. – Springer, 2015. – Vol. 9251.
– P. 222-230.
12. Turing A.M. On Computable Numbers, with an Application to the Entscheidungsproblem // Proceedings of the London Mathematical Society, 1937.
13. Abramovici M., Breuer M.A. and Friedman A.D. Digital Systems Testing and Testable Design. – Computer Science Press, 1990.
14. Hutter M. Convergence and Error Bounds for Universal Prediction of Nonbinary Sequences // Lecture Notes in Computer Science. – 2001. – Vol. 2167. – P. 239.
15. Курейчик В.М., Таран А.Е., Ляпунова И.А. Реализация муравьиного алгоритма на ГРИД-системе // Вестник Ростовского государственного университета путей сообщения.
– 2015. – № 4 (60). – С. 48-52.
16. Степанченко И.В. Методы тестирования программного обеспечения // РПК «Политехник». – Волгоград, 2006. – C. 75.
17. Сухинов А.И., Проценко Е.А., Чистяков А.Е., Шретер С.А. Сравнение вычислительных эффективностей явной и неявной схем для задачи транспорта наносов в прибрежных водных системах // Вычислительные методы и программирование: новые вычислительные технологии. – 2015. – Т. 16, № 3. – С. 328-338.
18. Малинин С.Н. Тестирование объектно-ориентированного программного обеспечения на основе моделирования конечными автоматами: дисс. … канд. техн. наук: 05.13.01.
– Нижний Новгород, 2010. – 156 с.
19. Отпущенников И.В. Методы и средства преобразования процедурных описаний дискретных функций в булевы уравнения: дисс. … канд. техн. наук: 05.13.11. – Иркутск, 2011. – 128 с.
20. Cegielski P., Richard D. On arithmetical first-order theories allowing encoding and decoding of lists // Theoretical Computer Science. – 1999. – Vol. 222, No. 1-2. – P. 55-75.
21. Emese Balogh, Anton Deguet, Robert C. Susi, Axel Krieger, Anand Viswanathan, Cynthia M´enard, Jonathan A. Coleman and Gabor Fichtinger. Visualization, Planning, and Monitoring Software for MRI-Guided Prostate Intervention Robot // Proceedings Lecture Notes in Computer Science. Springer. – Vol. 3217. – P. 73-80.
22. Beltran M., Castillo G., Kreinovich V. Algorithms That Still Produce a Solution (Maybe Not Optimal) Even When Interrupted: Shary's Idea Justified // Reliable Computing. – 1998. – Vol. 4, No. 1. – P. 39-53.

Comments are closed.