От редакторов выпуска.

Reflex — процесс-ориентированный язык, который обеспечивает разработку простого в обслуживании управляющего программного обеспечения для программируемых логических контроллеров. Язык был успешно использован в нескольких системах управления с повышенными требованиями к надежности, например, в системе управления печью для выращивания монокристаллов кремния и в комплексе контроля радиоэлектронной аппаратуры. В настоящее время основной целью языкового проекта Reflex является разработка методов формальной верификации для Reflex программ для того, чтобы гарантировать повышенную надежность создаваемого на его основе программного обеспечения. В статье представлена формальная операционная семантика Reflex программ, расширенных аннотациями, описывающими формальную спецификацию программных требований, как необходимый базис для применения таких методов. Дан краткий обзор языка Reflex и приведен простой пример его использования — управляющая программа для сушилки рук. Определены понятия окружения и переменных, разделяемых с окружением, позволяющие абстрагироваться от конкретных портов ввода/вывода. Определены типы аннотаций, задающие ограничения на значения переменных при запуске программы, ограничения на окружение (в частности, на объект управления), инварианты цикла управления, пред- и постусловия внешних функций, используемых в Reflex программах. Аннотированный Reflex также использует стандартные аннотации assume, assert и havoc. Операционная семантика аннотированных Reflex программ использует глобальные часы и локальные часы отдельных процессов, время которых измеряется в количестве итераций цикла управления, для моделирования временных ограничений на исполнение процессов в определенных состояниях. Она хранит полную историю изменений значений разделяемых переменных для более полного описания временных свойств программы и ее окружения. Семантика учитывает бесконечность цикла выполнения программы, логику управления переходами процессов из состояния в состояние и взаимодействие процессов между собой и с окружением. Расширение формальной операционной семантики языка Reflex на аннотации упрощает доказательство корректности разрабатываемого авторами трансформационного подхода к дедуктивной верификации Reflex программ, трансформирующего аннотированную Reflex программу к аннотированной программе на сильно ограниченном подмножестве языка C, за счет сведения сложного доказательства сохранения истинности требований к программе при трансформации к более простому доказательству эквивалентности исходной и результирующей аннотированных программ относительно их операционных семантик.

Во время набора высоты на больших пассажирских самолетах вертикальное движение самолета, то есть его угол наклона, зависит от угла отклонения руля высоты, выбранного пилотом. Если угол наклона становится слишком большим, самолет рискует нарушить воздушный поток на крыльях, что может привести к его падению. В некоторых самолетах пилоту помогает программное обеспечение, задачей которого является предотвращение нарушения воздушного потока. Когда угол наклона становится больше определенного порога, программное обеспечение отменяет решения пилота относительно угла отклонения руля высоты и обеспечивает предположительно безопасные значения. Хотя вспомогательное программное обеспечение может помочь предотвратить человеческие сбои, само программное обеспечение также подвержено ошибкам и, как правило, представляет собой риск для тщательной оценки. Например, если разработчики программного обеспечения забыли, что датчики могут давать неправильные данные, программное обеспечение может привести к тому, что угол наклона станет отрицательным. Следовательно, самолет теряет высоту и может – в конечном итоге – разбиться.

В этой статье мы представляем исполняемую модель, написанную на Matlab/Simulink® для системы управления пассажирским самолетом. Наша модель также учитывает программное обеспечение, помогающее пилоту предотвращать нарушение воздушного потока. При моделировании набора высоты с использованием нашей модели легко увидеть, что самолет может потерять высоту, если данные, предоставленные датчиком угла наклона, неверны. Для противоположного случая правильных данных датчика, моделирование предполагает, что система управления работает правильно и способна эффективно предотвращать нарушение воздушного потока.

Однако симуляция не является гарантией безопасности системы управления. По этой причине мы переводим Matlab/Simulink®-модель в гибридную программу (НР), т. е. во входной синтаксис средства доказательства теорем KeYmaera. Это открывает путь для формальной проверки свойств безопасности систем управления, смоделированных в Matlab/Simulink®. В качестве дополнительного вклада в эту статью мы обсудим текущие ограничения нашей трансформации. Например, оказывается, что простые пропорциональные (Р) контроллеры могут быть легко представлены программами НР, но более продвинутые контроллеры РD (пропорционально-производные) или РID (пропорционально-интегрально-производные) могут быть представлены как программы НР только в исключительных случаях.

В ИСИ СО РАН разрабатывается система C-lightVer для дедуктивной верификации С-программ. Исходя из двухуровневой архитектуры системы, входной язык C-light транслируется в промежуточный язык C-kernel. Метагенератор условий корректности принимает на вход C-kernel программу и логику Хоара для C-kernel. Для решения известной проблемы задания инвариантов циклов выбран подход финитных итераций. Тело цикла финитной итерации исполняется один раз для каждого элемента структуры данных конечной размерности, а правило вывода для них использует операцию замены rep, выражающую действие цикла в символической форме. Также в нашем метагенераторе внедрен и расширен метод семантической разметки условий корректности. Он позволяет порождать пояснения для недоказанных условий и упрощает локализацию ошибок. Наконец, если система ACL2 не справляется с установлением истинности условия, можно сосредоточиться на доказательстве его ложности. Ранее нами был разработан способ доказательства ложности условий корректности для системы ACL2. Необходимость в более подробных объяснениях условий корректности, содержащих операцию замены rep, привела к изменению алгоритмов генерации операции замены, извлечения семантических меток и генерации объяснений недоказанных условий корректности. В статье представлены модификации данных алгоритмов. Эти изменения позволяют пометить исходный код функции rep семантическими метками, извлекать семантические метки из определения rep, а также генерировать описание условия исполнения инструкции break.

В течение многих лет автомобильные встраиваемые системы проверялись только тестированием. В ближайшем будущем усовершенствованные системы помощи водителю (ADAS) будут играть большую роль в дизайне и разработке программного обеспечения автомобиля. Кроме того, увеличение их критического уровня может привести к тому, что власти потребуют сертификации этих систем. Мы думаем, что привнесение формальных доказательств в их развитие может помочь обеспечить выполнение свойств безопасности и получить эффективный процесс сертификации. Другие отрасли (например, аэрокосмическая, железнодорожная, ядерная), которые создают критические системы, требующие сертификации, также могут быть заинтересованы в развитии формальных методов проверки. Одним из этих методов является дедуктивное доказательство. Это может дать более высокий уровень уверенности в доказательстве критических свойств безопасности и даже избежать модульное тестирование. В этой статье мы выбрали вариант прикладного использования: функцию, вычисляющую квадратный корень с помощью линейной интерполяции. Мы используем дедуктивное доказательство, чтобы доказать его правильность и показать ограничения, с которыми мы сталкиваемся при работе с готовыми инструментами. Мы предлагаем подходы для преодоления некоторых ограничений, связанных с этими инструментами, чтобы преуспеть с доказательством. Эти подходы могут быть применены к аналогичным проблемам, которые часто встречаются в автомобильном встроенном программном обеспечении.

Удобная для пользователя формальная спецификация и верификация параллельных и распределённых систем, принадлежащих различным предметным областям, таким как системы автоматического управления, телекоммуникации, бизнес-процессы, являются активными темами исследований в силу их практической значимости. В этой статье мы представляем методы разработки специализированных ориентированных на верификацию онтологий процессов, которые используются для описания параллельных и распределенных систем предметных областей. Одним из преимуществ таких онтологий является их формальная семантика, которая делает возможной формальную верификацию описанных систем. Наш метод основан на абстрактной онтологии процессов, ориентированной на верификацию. Мы используем два метода специализации абстрактной онтологии процессов. Декларативный метод с помощью специализации классов исходной онтологии, введения новых декларативных классов, а также системы аксиом задаёт ограничения для классов и отношений абстрактной онтологии. Конструктивный метод использует техники семантической разметки и сопоставления с образцом, чтобы связать понятия предметной области с классами абстрактной онтологии процессов. Мы даём подробные онтологические спецификации этих техник. Наши методы сохраняют формальную семантику исходной онтологии процессов и, следовательно, возможность применения формальных методов верификации к специализированным онтологиям процессов. Мы показываем, что конструктивный метод является уточнением декларативного метода. Построение онтологии типовых элементов систем автоматического управления иллюстрирует наши методы: разработано декларативное описание классов и ограничений специализированной онтологии в системе Protege на языке OWL с использованием правил вывода на языке SWRL и построена система шаблонов семантической разметки, которая реализует типовые элементы систем автоматического управления.

Достижимость, направляемая свойством, (Property Directed Reachability, PDR) — эффективный и масштабируемый подход к решению систем символьных ограничений, известных как дизъюнкты Хорна с ограничениями (Constrained Horn Clauses, CHC). В случае нелинейных систем дизъюнктов, которые могут возникнуть, к примеру, из задач реляционной верификации, PDR выводит индуктивные инварианты для каждого неинтерпретированного предикатного символа. Тем не менее на практике автоматический вывод таких решений не удаётся, т.к. инварианты должны выводиться для групп предикатных символов вместо индивидуальных предикатных символов. В статье описан новый алгоритм, автоматически определяющий такие группы и обобщающий существующий подход PDR. Ключевая особенность алгоритма состоит в том, что он не требует потенциально дорогой синхронизирующей трансформации системы дизъюнктов Хорна. Алгоритм был реализован над современным решателем дизъюнктов Хорна Spacer. Эксперименты показывают, что полученная реализация успешно выводит реляционные инварианты для некоторых систем дизъюнктов, на которых существующие решатели не завершаются.

Рассматривается вычислительная реализация алгоритма оценки спектра показателей Ляпунова для систем дифференциальных уравнений с запаздывающими аргументами. Учитывая, что для таких систем, а также для краевых задач не удается доказать известную теорему Оселедеца, которая позволяет эффективно вычислять искомые величины, приходится говорить лишь об оценках характеристических показателей, в каком-то смысле близких к ляпуновским. В данной работе предложены две методики обработки решений линеаризованных на аттракторе систем, одна из которых основана на базисе импульсных функций, а другая — на базисе тригонометрических функций. Продемонстрирована гибкость применения указанных алгоритмов в случае квазиустойчивых структур, когда несколько показателей Ляпунова близки к нулю. Разработанные методы тестируются на логистическом уравнении с запаздыванием. Полученные результаты иллюстрируют “близость” оцениваемых характеристик и показателей Ляпунова.