| Название НИОКТР |
Развитие формальных и экспериментальных методов повышения надежности сложных динамических систем на базе обобщенных автоматных, логических и онтологических моделей
|
| Аннотация |
Стремительный рост размеров и сложности программного обеспечения делает вопрос его корректности критически важным. Индустрия делает определенные шаги в виде более широкого применения языков программирования с более безопасной моделью памяти (C#, Go, Rust и др.) и введения контрактов в стандартные определения языков. Тем не менее, до сих пор основным инструментом проверки программ остается трудоемкое тестирование, при этом не гарантирующее полной корректности. Там же, где академические коллективы пытаются внедрять более строгие методы, часто ограничиваются классическим логиками и исчислениями, не всегда пригодными для современных программ.
Данный проект направлен на разработку и внедрение формальных методов проверки свойств программ, математически и логически обоснованных и корректных. Особенно подчеркнем необходимость разработки инструментальных средств поддержки, частично снимающих с массовых программистов задачу глубокого освоения фундаментальных теорий. Выделим основные направления планируемых работ.
1. Исследования в области параллельных и мультиагентных систем: построение исчисления дискретно-временных фазовых боксов Петри dtphPBC – стохастической процессной алгебры (СПА) с задержками фазового типа; конструирование параллельной структурной операционной семантики исчисления на помеченных стохастических системах переходов и композициональной семантики на помеченных дискретно-временных фазовых стохастических сетях Петри; доказательство согласованности операционной и композициональной семантик dtphPBC относительно новой шаговой фазовой бисимуляционной эквивалентности и ее сравнение по различающей способности с другими семантическими эквивалентностями; построение, исследование и обоснование семантик в спектре «интерливинг/«истинный параллелизм» и эквивалентностей в спектре «линейное/ветвящееся время» в контексте различных классов реверсивных сетей Петри и событийно-ориентированных моделей; исследование границ применения методов средств и методов проверки моделей для теоретической оценки производительности исполнения высоконагруженных вычислений на ряде современных GPU и CPU процессоров; исследование формализации различных форм знаний в мультиагентных системах с использованием логик знаний и действий, в частности формализация и верификация знаний агентов о последовательностях действий других агентов системы.
2. Исследования в области семантик языков программирования и дедуктивной верификации программ: разработка единой логики для доказательства корректности и некорректности программ с финитными итерациями над массивами; проверка работоспособности системы дедуктивной верификации C-lightVer на коллекции задач с серии всероссийских соревнований VeHa по формальной верификации программ; разработка методов и инструментов верификации императивных программ, основанных на комбинации операционного, трансформационного, дедуктивного и онтологического подходов к спецификации семантик программ.
3. Исследования в области неклассических логик: выработка семантического аппарата на базе Систем Крипке для временных и модальных логик и алгоритмы проверки истинности информации и разрешимости в них; исследование допустимых и истинных правил вывода для построенных логических систем; изучение проблем унификации и построения унификационных базисов на базе техники проективных формул.
4. Расширение формальных методов для дискретных систем на случай непрерывных данных: исследование порядково позитивных полей с использованием теоретико-модельных методов и оснований вычислимого анализа; построение развитой теории вычислений на топологических структурах (таких как вещественные числа или функциональные пространства), основанной на логических, топологических и структурных методах анализа вычислительных задач.
|
| Доступ к ОКОГУ исполнителя |
False
|
| Количество связанных РИД |
0
|
| Количество завершенных ИКРБС |
0
|
| Сумма бюджета |
90372.028
|
| Дата начала |
2026-01-01
|
| Дата окончания |
2030-12-31
|
| Номер контракта |
075-00331-26-00
|
| Дата контракта |
2026-01-12
|
| Количество отчетов |
5
|
| УДК |
2;141.45
|
| Количество просмотров |
1
|
| Руководитель работы |
Вирбицкайте Ирина Бонавентуровна
|
| Руководитель организации |
Пальянов Андрей Юрьевич
|
| Исполнитель |
ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ БЮДЖЕТНОЕ УЧРЕЖДЕНИЕ НАУКИ ИНСТИТУТ СИСТЕМ ИНФОРМАТИКИ ИМ. А.П. ЕРШОВА СИБИРСКОГО ОТДЕЛЕНИЯ РОССИЙСКОЙ АКАДЕМИИ НАУК
|
| Заказчик |
МИНИСТЕРСТВО НАУКИ И ВЫСШЕГО ОБРАЗОВАНИЯ РОССИЙСКОЙ ФЕДЕРАЦИИ
|
| Федеральная программа |
Отсутствует
|
| Госпрограмма |
Фундаментальные и поисковые научные исследования
|
| Основание НИОКТР |
Государственное задание
|
| Последний статус |
2026-02-06 14:31:24 UTC, 2026-02-06 14:31:24 UTC
|
| ОКПД |
Услуги (работы), связанные с научными исследованиями и экспериментальными разработками в области технических наук и в области технологий, прочие, не включенные в другие группировки, кроме биотехнологии
|
| Отраслевой сегмент |
—
|
| Минздрав |
—
|
| Межгосударственная целевая программа |
—
|
| Ключевые слова |
дедуктивная верификация императивных программ; сети Петри; языки dREAL, SDL, Go (Golang), Promela, ASL; алгебраические, вычислительные и сложностные характеристики порядково-позитивных полей; моделирование распределённых систем; трансформационная семантика; онтологическое моделирование; реверсивные модели параллельных процессов; неклассические логики; трансляция спецификаций
|
| Соисполнители |
—
|
| Типы НИОКТР |
Фундаментальное исследование
|
| Приоритетные направления |
—
|
| Критические технологии |
—
|
| Рубрикатор |
50.41.23 - Программное обеспечение вычислительных сетей; 50.05.17 - Теоретические основы системного программного обеспечения; 28.25.23 - Кибернетические аспекты структурно-логической теории алгоритмов и программирования; 28.15.15 - Линейные детерминированные системы; 27.03.02 - Общие проблемы математической логики и основания математики
|
| OECD |
—
|
| OESR |
Компьютерные, информационные науки и биоинформатика (разработка аппаратного обеспечения относится к разделу 2.2, социальный аспект относится к разделу 5.8)
|
| Приоритеты научно-технического развития |
а) переход к передовым технологиям проектирования и создания высокотехнологичной продукции, основанным на применении интеллектуальных производственных решений, роботизированных и высокопроизводительных вычислительных систем, новых материалов и химических соединений, результатов обработки больших объемов данных, технологий машинного обучения и искусственного интеллекта;
|
| Регистрационные номера |
—
|
