Модель памяти описывает требования консистентности памяти в многопоточной системе. Оптимизации компилятора могут нарушить требования консистентности из-за ошибок, и поведение программы будет отличаться от требуемого. Ошибки в оптимизациях компилятора, например, некорректную перестановку инструкций, очень сложно обнаружить, так как они могут возникать с очень небольшим шансом при реальном исполнении. Существуют различные подходы формальной верификации требований консистентности памяти, однако основная сложность состоит в том, что данные подходы не масшабируются на промышленное программное обеспечение. В данное работе представлен инструмент MCC, который был успешно апробирован на виртуальной машине ARK VM и обнаружил реальную ошибку в оптимизации компилятора. Инструмент MCC является статическим, что позволяет проверить все возможные выполнения конкретной тестовой программы, не полагаясь на реальной выполнение на определенной архитектуре. Подход также включает в себя генерацию тестов и спецификацию проверяемых свойств.
Процессно-ориентированное программирование - перспективный подход к разработке управляющего программного обеспечения. Управляющее программное обеспечение часто требует высокой надежности. Формальные методы верификации, в частности дедуктивная верификация, используются для доказательства правильности таких программ относительно требований. Ранее был разработан язык темпоральных требований чтобы специфицировать темпоральные требования для дедуктивной верификации процесс-ориентированных программ. Было также показано, что значительная часть требований относится к небольшому числу классов. Для этих классов были разработаны шаблоны требований. В данной статье мы представляем коллекцию процесс-ориентированных программ и требований к ним. Требования формализованы на языке темпоральных требований и классифицированы в соответствии с набором шаблонов. Мы также определяем новый шаблон требований. Эти результаты могут быть использованы при исследовании формальных методов верификации процесс-ориентированных программ, в частности, при исследовании методов доказательства условий корректности.
Процесс-ориентированное программирование является парадигмой, основанной на понятии процесса, где каждый процесс внутри является параллельным автоматом. Парадигма предназначена для разработчиков ПЛК (программируемых логических контроллеров) чтобы писать программное обеспечение для Industry 4.0.
Язык poST - перспективное процесс-ориентированное расширение языка структурированного текста (ST) стандарта IEC 61131-3, обеспечивающее концептуальную согласованность исходного кода ПЛК с технологическим описанием управляемого процесса. Этот язык сочетает преимущества автоматного программирования со стандартным синтаксисом языка ST. Мы предлагаем трансформационную семантику poST, содержащую правила трансляции poST-операторов в Promela – входной язык системы проверки моделей SPIN. Следуя этим семантическим правилам, наш транслятор, основанный на Xtext, порождает модель на языке Promela для poST-программы.
Нашим вкладом является метод автоматической генерации кода на языке Promela из управляющих программ на языке poST. Полученная в результате Promela-программа может быть верифицирована с помощью системы SPIN относительно требований к исходной программе poST на языке линейной темпоральной логики LTL.
SSA-форма – промежуточное представление для компиляции императивных программ, где каждой переменной значение присваивается лишь единожды. Будучи правильно определённой, SSA-форма порождает семейство чисто синтаксических категорий с несколькими хорошими свойствами. Мы надеемся, что эта работа послужит основанием для категорного подхода к оптимизации.
Генеративные системы искусственного интеллекта должны тщательно тестироваться, поскольку они могут создавать данные плохого качества, однако процесс тестирования осложняется проблемой тестового оракула. Тестирование инвариантами помогает тестировать программы без тестового оракула. В этом исследовании мы рассматриваем систему ИИ для создания персонализированных стикеров. Персонализированный стикер - это тематическая картинка с лицом человека, декоративными элементами и надписями. Данная система состоит из многих компонент и является стохастической. Мы определили требования для системы целиком и проверили их с помощью тестовых инвариантов. Эти требования регулируют зависимости от качества входных изображений и итоговое качество создаваемых стикеров. Наша методика помогла обнаружить значительные проблемы в тестируемой системе.
В статье представлена текущая реализация языкового сервера для интерактивного доказателя теорем Rzk. Она анализирует соответствующие технологии, связанные с языковым сервером Protocol, расширениями VS Code и доказателями теорем, и как на их основе строится языковая поддержка для Rzk.