Применение статического анализа для сокращения количества порождаемых условий корректности для программ на языке Reflex

Применение статического анализа для сокращения количества порождаемых условий корректности для программ на языке Reflex

Ищенко А.Д. (ИАиЭ СО РАН, Новосибирск, Россия)
Ануреев И.С. (ИАиЭ СО РАН, Новосибирск, Россия)

Аннотация

Системы управления широко применяются в критически важных областях, что предъявляет повышенные требования к надежности программного обеспечения для таких систем и к обоснованию его корректности. Для выполнения этих требований используют формальные методы, в частности дедуктивную верификацию, которая предполагает генерацию условий корректности на основе аксиоматической семантики программы и ее спецификаций. Однако автоматическая генерация условий корректности нередко приводит к появлению избыточных и/или чрезмерно сложных формул, что затрудняет их последующую проверку и снижает эффективность автоматических доказателей. Частично эту проблему решают предметно-ориентированные языки, такие как Reflex, который использует процесс-ориентированную парадигму, упрощающую структуру программ. Вместе с тем особенности семантики конструкций Reflex могут вызывать дополнительный рост числа условий корректности за счет нерелевантных условий корректности, соответствующих недостижимым путям в программе. В работе предлагается метод статического анализа, направленный на сокращение числа генерируемых условий корректности для программ на языке Reflex. Метод основан на аннотировании операторов программы набором атрибутов, отражающих их семантические свойства. Сначала атрибуты вычисляются для элементарных операторов, а затем агрегируются для составных конструкций. В процессе генерации условий корректности атрибуты накапливаются вдоль пройденного пути выполнения, после чего проверяется их совместность. Несовместимые комбинации атрибутов позволяют выявлять и отбрасывать нерелевантные условия корректности. Экспериментальная оценка на наборе тестовых программ показала, что предложенный подход позволяет существенно сократить количество условий корректности (до 97% в отдельных случаях), причем эффективность метода растет с увеличением числа процессов и состояний в программе.

Ключевые слова

язык Reflex; процесс-ориентированное программирование; условия корректности; статический анализ; атрибуты

Издание

Труды Института системного программирования РАН, том 38, вып. 6, часть 2, 2026, стр. 21-40.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(6)-23

Для цитирования

Ищенко А.Д., Ануреев И.С. Применение статического анализа для сокращения количества порождаемых условий корректности для программ на языке Reflex. Труды Института системного программирования РАН, том 38, вып. 6, часть 2, 2026, стр. 21-40. DOI: 10.15514/ISPRAS-2026-38(6)-23.

Полный текст статьи в формате pdf Вернуться к содержанию тома