Editorials
Computing Methodologies and Applications
Reflex — процесс-ориентированный язык, который обеспечивает разработку простого в обслуживании управляющего программного обеспечения для программируемых логических контроллеров. Язык был успешно использован в нескольких системах управления с повышенными требованиями к надежности, например, в системе управления печью для выращивания монокристаллов кремния и в комплексе контроля радиоэлектронной аппаратуры. В настоящее время основной целью языкового проекта Reflex является разработка методов формальной верификации для Reflex программ для того, чтобы гарантировать повышенную надежность создаваемого на его основе программного обеспечения. В статье представлена формальная операционная семантика Reflex программ, расширенных аннотациями, описывающими формальную спецификацию программных требований, как необходимый базис для применения таких методов. Дан краткий обзор языка Reflex и приведен простой пример его использования — управляющая программа для сушилки рук. Определены понятия окружения и переменных, разделяемых с окружением, позволяющие абстрагироваться от конкретных портов ввода/вывода. Определены типы аннотаций, задающие ограничения на значения переменных при запуске программы, ограничения на окружение (в частности, на объект управления), инварианты цикла управления, пред- и постусловия внешних функций, используемых в Reflex программах. Аннотированный Reflex также использует стандартные аннотации assume, assert и havoc. Операционная семантика аннотированных Reflex программ использует глобальные часы и локальные часы отдельных процессов, время которых измеряется в количестве итераций цикла управления, для моделирования временных ограничений на исполнение процессов в определенных состояниях. Она хранит полную историю изменений значений разделяемых переменных для более полного описания временных свойств программы и ее окружения. Семантика учитывает бесконечность цикла выполнения программы, логику управления переходами процессов из состояния в состояние и взаимодействие процессов между собой и с окружением. Расширение формальной операционной семантики языка Reflex на аннотации упрощает доказательство корректности разрабатываемого авторами трансформационного подхода к дедуктивной верификации Reflex программ, трансформирующего аннотированную Reflex программу к аннотированной программе на сильно ограниченном подмножестве языка C, за счет сведения сложного доказательства сохранения истинности требований к программе при трансформации к более простому доказательству эквивалентности исходной и результирующей аннотированных программ относительно их операционных семантик.
Во время набора высоты на больших пассажирских самолетах вертикальное движение самолета, то есть его угол наклона, зависит от угла отклонения руля высоты, выбранного пилотом. Если угол наклона становится слишком большим, самолет рискует нарушить воздушный поток на крыльях, что может привести к его падению. В некоторых самолетах пилоту помогает программное обеспечение, задачей которого является предотвращение нарушения воздушного потока. Когда угол наклона становится больше определенного порога, программное обеспечение отменяет решения пилота относительно угла отклонения руля высоты и обеспечивает предположительно безопасные значения. Хотя вспомогательное программное обеспечение может помочь предотвратить человеческие сбои, само программное обеспечение также подвержено ошибкам и, как правило, представляет собой риск для тщательной оценки. Например, если разработчики программного обеспечения забыли, что датчики могут давать неправильные данные, программное обеспечение может привести к тому, что угол наклона станет отрицательным. Следовательно, самолет теряет высоту и может – в конечном итоге – разбиться.
В этой статье мы представляем исполняемую модель, написанную на Matlab/Simulink® для системы управления пассажирским самолетом. Наша модель также учитывает программное обеспечение, помогающее пилоту предотвращать нарушение воздушного потока. При моделировании набора высоты с использованием нашей модели легко увидеть, что самолет может потерять высоту, если данные, предоставленные датчиком угла наклона, неверны. Для противоположного случая правильных данных датчика, моделирование предполагает, что система управления работает правильно и способна эффективно предотвращать нарушение воздушного потока.
Однако симуляция не является гарантией безопасности системы управления. По этой причине мы переводим Matlab/Simulink®-модель в гибридную программу (НР), т. е. во входной синтаксис средства доказательства теорем KeYmaera. Это открывает путь для формальной проверки свойств безопасности систем управления, смоделированных в Matlab/Simulink®. В качестве дополнительного вклада в эту статью мы обсудим текущие ограничения нашей трансформации. Например, оказывается, что простые пропорциональные (Р) контроллеры могут быть легко представлены программами НР, но более продвинутые контроллеры РD (пропорционально-производные) или РID (пропорционально-интегрально-производные) могут быть представлены как программы НР только в исключительных случаях.
В течение многих лет автомобильные встраиваемые системы проверялись только тестированием. В ближайшем будущем усовершенствованные системы помощи водителю (ADAS) будут играть большую роль в дизайне и разработке программного обеспечения автомобиля. Кроме того, увеличение их критического уровня может привести к тому, что власти потребуют сертификации этих систем. Мы думаем, что привнесение формальных доказательств в их развитие может помочь обеспечить выполнение свойств безопасности и получить эффективный процесс сертификации. Другие отрасли (например, аэрокосмическая, железнодорожная, ядерная), которые создают критические системы, требующие сертификации, также могут быть заинтересованы в развитии формальных методов проверки. Одним из этих методов является дедуктивное доказательство. Это может дать более высокий уровень уверенности в доказательстве критических свойств безопасности и даже избежать модульное тестирование. В этой статье мы выбрали вариант прикладного использования: функцию, вычисляющую квадратный корень с помощью линейной интерполяции. Мы используем дедуктивное доказательство, чтобы доказать его правильность и показать ограничения, с которыми мы сталкиваемся при работе с готовыми инструментами. Мы предлагаем подходы для преодоления некоторых ограничений, связанных с этими инструментами, чтобы преуспеть с доказательством. Эти подходы могут быть применены к аналогичным проблемам, которые часто встречаются в автомобильном встроенном программном обеспечении.
Theory of Data
Algorithms
Computer System Organization
ISSN 2313-5417 (Online)