![]() |
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
Проблема снижения количества различного рода ошибок в программном обеспечении, особенно — в критически важном, путём его верификации и валидации сейчас крайне актуальна. Применение методов формальной верификации, целью которых является получение строгих математических доказательств того, что программа удовлетворяет предъявляемым к ней требованиям, на практике ограничено. Это обстоятельство, в первую очередь, связано с наукоёмкостью и, как правило, трудозатратным характером существующих методов формальной верификации, а также со сложностью языков программирования, которые традиционно используются при разработке подобных программных комплексов. В рамках проекта предполагается разработка методов формальной верификации кода, основанных на языково-ориентированном программировании. В рамках этого подхода при разработке программных комплексов декомпозиция осуществляется, в первую очередь, путём создания набора специализированных языков программирования, адекватно отражающих специфику предметной области (предметно-ориентированных языков). По сравнению с языками программирования общего назначения, предметно-ориентированные языки могут иметь более простую семантику, упрощающую задачу формальной верификации программ на таких языках. Подобные языки, в частности, могут разрабатываться с заданной формальной семантикой на основе существующих или вновь создаваемых математических моделей, отражающих знания о той или иной области приложения программ. Применение таких методов, начиная с ранних этапов жизненного цикла программного продукта, особенно при разработке его макета на этапе предпроектных исследований, позволяет создавать эффективные формальные спецификации программ и поддерживать процедуры их валидации.
грант РФФИ |
# | Сроки | Название |
1 | 1 января 2016 г.-31 декабря 2016 г. | Получение промежуточного представления и разработка макетов средств для работы с таким представлением |
Результаты этапа: | ||
2 | 1 января 2017 г.-31 декабря 2017 г. | Разработка методов описания формальной семантики предметно-ориентированных языков |
Результаты этапа: 1. Система типов промежуточного представления расширена дополнительными достаточными условиями завершимости функции, а именно: - отсутствие рекурсивного вызова; - наличие рекурсивного вызова, для которого мера длины входной цепочки строго убывает при переходе по графу вызовов; - наличие рекурсивного вызова, для которого при некоторой заданной мере (завершимой функции из входных аргументов исходной функции в натуральные числа), значение меры на входной цепочке строго убывает при переходе по графу вызовов. 2. Макет программного средства проверки типов расширен для поддержки проверки условий завершимости функции с учётом их аннотации используемым достаточным условием. 3. Реализованы методы описания формальной семантики предметно- ориентированных языков в терминах промежуточного представления. Формальная семантика описывается как последовательное приближение типа функции от наиболее общего, соответствующего λ-исчислению с простыми типами, до наиболее точного, соответствующего коду функции в промежуточном представлении. Семантика предметно-ориентированных языков описывается в виде интерпретатора или транслятора предложений языка в промежуточном представлении. 4. В форме предметно-ориентированного языка с заданной формальной семантикой реализован способ описания синтаксиса, полученный при решении задачи 1.5. Для описания синтаксиса используется подход на основе типизрованных комбинаторов парсеров | ||
3 | 1 января 2018 г.-31 декабря 2018 г. | Разработка методов описания формальной семантики предметно-ориентированных языков |
Результаты этапа: Общей целью проекта на весь срок исследований по проекту являлась разработка методов и реализующих их программных средств, которые, в свою очередь, предназначены для спецификации и разработки сложных наукоёмких программных комплексов с использованием языков программирования, адекватно отражающих специфику предметной области (предметно-ориентированных языков), а также для получения формального, проверяемого алгоритмически доказательства соответствия программ таким спецификациям. В ходе проекта получены следующие основные результаты. 1. Разработано промежуточное представление для описания семантики предметно-ориентированных языков. 2. Реализован макет программного средства проверки типов (спецификаций) для подмножества промежуточного представления. 3. Обоснована возможность реализации методов для автоматизации процесса верификации программ, написанных на предметно-ориентированных языках. 4. Разработан макет библиотек программных модулей для описания синтаксиса предметно-ориентированных языков и их трансляции в промежуточное представление. 5. Для иллюстрации предлагаемого подхода разработан набор предметно-ориентированных языков для описания фрагмента реализации функциональных возможностей сложно организованных информационно-аналитических систем. |
Для прикрепления результата сначала выберете тип результата (статьи, книги, ...). После чего введите несколько символов в поле поиска прикрепляемого результата, затем выберете один из предложенных и нажмите кнопку "Добавить".