Безопасность цифровых технологий

БЕЗОПАСНОСТЬ ЦИФРОВЫХ ТЕХНОЛОГИЙ

БЕЗОПАСНОСТЬ
ЦИФРОВЫХ ТЕХНОЛОГИЙ

English | Русский

Последний выпуск
№2(2025) Апрель - Июнь 2025

Сравнение методов преобразования программного цикла с использованием символьной нотации

Выпуск № 1 (79) Январь - Март 2015
Авторы:

А.А. ВОЕВОДА,
Д.О. РОМАННИКОВ
DOI: http://dx.doi.org/10.17212/2307-6879-2015-1-65-76
Аннотация
Современные технические системы – это, возможно, одни из самых сложных технических систем во всей человеческой деятельности. На сегодняшний день такие системы чаще всего состоят из интеграции программной и аппаратной частей. При этом рост сложности самой системы приводит к значительному увеличению сложности разработки и контроля за качеством программной системы. На сегодняшний день в индустрии разработки программного обеспечения нет формальных средств, которые могли бы гарантировать отсутствие программных ошибок. Большое влияние на сложность программного анализа оказывает значительное увеличение программных путей, в особенности из-за наличия условных операторов в циклах. В данной статье рассматривается подход уменьшения количества программных путей, который основан на символьной нотации. Согласно данному подходу программный цикл должен быть представлен как символьное выражение, которое определяет переменные ив котором условные операторы представлены в виде дополнительных переменных. После этого программа должна быть представлена в виде дерева с вершинами в виде контекстов. Далее полученное дерево контекстов может быть проанализировано в любом состоянии путем вычисления выражения, в котором содержатся возможные значения переменных вместо их символьного представления. Статья завершается формулированием общего алгоритма анализа программы. Задача получения формального алгоритма преобразования цикла является темой отдельного исследования и будет рассмотрена в последующих работах, также как и представление математического аппарата для вычисления возможных значений символьных выражений при подстановке в него возможных значений переменных.

 
Ключевые слова: программное обеспечение, тестирование, входные интервалы, формальная верификация, динамическая верификация, верификация, проверка моделей, модели программного обеспечения, графы, тотальная корректность программ
Просмотров: 2684