Приглашаем к участию в новом номере журнала "Системная информатика"

Уважаемые коллеги!

Приглашаем вас прислать статью в номер 22 журнала "Системная информатика". Номер выйдет 15 декабря.

Преимущества журнала: большой объем статьи (до 50-60 страниц), использование цветных шрифтов и иллюстраций, публикации на русском и английском языках, быстрая публикация статьи.


О журнале

Научный электронный журнал "Системная информатика" основан в 2013 году.

Учредитель - Федеральное государственное бюджетное учреждение науки Институт систем информатики им. А.П. Ершова Сибирского отделения Российской академии наук.

Свидетельство о государственной регистрации СМИ - ЭЛ № ФС 77-55164.

Свидетельство выдано Федеральной службой по надзору в сфере связи, информационных технологий и массовых коммуникаций.

В журнале публикуются научные статьи по информатике, программированию и информационным технологиям. Статьи подлежат обязательному рецензированию членами редколлегии журнала.

Читать дальше

Скачать выпуск целиком (2.82 МБ)
Скачать

Проверка корректности модели памяти методами статического анализа

Андрианов Павел Сергеевич, Мутилин Вадим Сергеевич
Модель памяти описывает требования консистентности памяти в многопоточной системе. Оптимизации компилятора могут нарушить требования консистентности из-за ошибок, и поведение программы будет отличаться от требуемого. Ошибки в оптимизациях компилятора, например, некорректную перестановку инструкций, очень сложно обнаружить, так как они могут возникать с очень небольшим шансом при реальном исполнении. Существуют различные подходы...
статический анализ, модель памяти, оптимизации компилятора
Скачать

Шаблоны требований, возникающих при дедуктивной верификации процесс-ориентированных программ, и примеры их использования

Черненко Иван Михайлович
Процессно-ориентированное программирование - перспективный подход к разработке управляющего программного обеспечения. Управляющее программное обеспечение часто требует высокой надежности. Формальные методы верификации, в частности дедуктивная верификация, используются для доказательства правильности таких программ относительно требований. Ранее был разработан язык темпоральных требований чтобы специфицировать темпоральные требования для дедуктивной верификации процесс-ориентированных программ. Было также показано...
дедуктивная верификация, темпоральные требования, управляющее программное обеспечение, процесс-ориентированные программы
Скачать

Верификация моделей программ на процесс-ориентированном расширении языка Structured Text стандарта IEC 61131-3

Гаранина Наталья Олеговна, Старолетов Сергей Михайлович, Зюбин Владимир Евгеньевич, Ануреев Игорь Сергеевич
Процесс-ориентированное программирование является парадигмой, основанной на понятии процесса, где каждый процесс внутри является параллельным автоматом. Парадигма предназначена для разработчиков ПЛК (программируемых логических контроллеров) чтобы писать программное обеспечение для Industry 4.0. Язык poST - перспективное процесс-ориентированное расширение языка структурированного текста (ST) стандарта IEC 61131-3, обеспечивающее концептуальную согласованность исходного кода ПЛК с...
управляющее программное обеспечение, проверка моделей, процесс-ориентированное программирование, LTL, SPIN, Structured Text
Скачать

Алгебры SSA

Соколов Павел Павлович
SSA-форма – промежуточное представление для компиляции императивных программ, где каждой переменной значение присваивается лишь единожды. Будучи правильно определённой, SSA-форма порождает семейство чисто синтаксических категорий с несколькими хорошими свойствами. Мы надеемся, что эта работа послужит основанием для категорного подхода к оптимизации.
формализмы для семантик программ, теория категорий, синтез и преобразование программ
Скачать

Тестирование инвариантами в применении к генеративным системам искусственного интеллекта

Якушева Софья Федоровна, Хританков Антон Сергеевич, Горбачёнок Дарья Игоревна
Генеративные системы искусственного интеллекта должны тщательно тестироваться, поскольку они могут создавать данные плохого качества, однако процесс тестирования осложняется проблемой тестового оракула. Тестирование инвариантами помогает тестировать программы без тестового оракула. В этом исследовании мы рассматриваем систему ИИ для создания персонализированных стикеров. Персонализированный стикер - это тематическая картинка с лицом человека, декоративными...
тестирование инвариантами, генеративные системы искусственного интеллекта, контроль качества программного обеспечения
Скачать

Реализация языкового сервера для интерактивного доказателя теорем Rzk

Абунегм Абдельрахман Али Хассанеин, Кудасов Николай Дмитриевич
В статье представлена текущая реализация языкового сервера для интерактивного доказателя теорем Rzk. Она анализирует соответствующие технологии, связанные с языковым сервером Protocol, расширениями VS Code и доказателями теорем, и как на их основе строится языковая поддержка для Rzk.
протокол языкового сервера, расширение Visual Studio Code, доказатель теорем, гомотопическая теория типа, теория категорий