Анализ моделей проектирования системы с использованием технологии проверки моделей является важным шагом в процессе проектирования системы.
Она позволяет проводить автоматизированную сверку свойств системы с заданными моделями конструкции. Автоматизированный характер проверки модели облегчает интеграцию верификационного этапа в процесс проектирования, поскольку не требует дополнительного вмешательства проектировщика после того, как модель была сформулирована и свойство было указано.
Часто бывает достаточно абстрагироваться от аспектов реального времени при проверке свойств системы, в частности, когда внимание сосредоточено на функциональных аспектах системы. Однако, когда нефункциональные свойства, такие как время отклика или время периодического поведения, играют важную роль, необходимо включать аспекты реального времени в модели и спецификацию, а также использовать специализированные инструменты проверки моделей в режиме реального времени, такие как UPPAAL, Kronos или Opaal на этапе проверки.
Помимо автоматической природы проверки модели, возможность возврата контр примеров в режиме реального времени является еще одним практическим преимуществом использования технологии проверки модели, часто называемой временной диагностической трассой (TDT).
TDT описывает хронологическую последовательность шагов, которая переводит проектную модель из начального состояния системы в состояние, нарушающее свойство реального времени. ТДТ не является ни причинно-следственным объяснением нарушения прав собственности, ни подсказкой о том, как исправить модель.
В данной статье описываю автоматизированный метод расчета предложений по возможному ремонту сети синхронизированных автоматов (АСУТП), который позволяет избежать нарушения свойства безопасности с заданным временем.
Рассмотрим ТДТ, изображенную на рис. 1 в виде временной аннотированной последовательности. Этот сценарий описывает простой обмен сообщениями, при котором процесс dbServer посылает запрос на обработку db и они после некоторых шагов обработки, возвращает сообщение ser на dbServer.
Предположим, что система требует, чтобы время от отправки ответа до получения ответа не превышало 4-х временных единиц. Предположим, что аннотации временных интервалов на диаграмме последовательности представляют собой минимальное и максимальное время для шагов передачи и обработки сообщений, и допускает НТА, на основе которого была построена диаграмма.
Ремонт
Предлагаю методику ремонта, которая анализирует ответственность значений тактовых импульсов, возникающих в одном TDT, за нарушение спецификации. Анализ предполагает возможный синтаксический ремонт. На втором этапе определяем тест приемлемости, который оценивает допустимость ремонта в контексте полной модели ТА.
Вариация с привязкой к часам. Введем связанные вариационные переменные v это означает корректирующие значения, которые исправление добавит к границам часов, возникающим в инвариантах местоположения и в защитных переходах. Значения выбираются так, чтобы ни одна из реализаций S в модифицированном автомате все еще не являлась свидетелем нарушения Π , Это делается путем определения новой системы ограничений, которая фиксирует условия переменной v при котором нарушение Π не появится в соответствующем следе модифицированного автомата. Используя эту систему ограничений, мы затем определяем задачу максимальной выполнимости, решение которой сводит к минимуму количество изменений в T , необходимых для достижения ремонта.
Часы границы , происходящие в инвариантов расположения и в переходных охранниками, представлены ibounds и GBounds множеств , определенных для TDT S . Обратите внимание, что каждая переменная часов c может быть связана с мс , л различные границы часов в инварианте местоположения l , обозначаемые множеством Открыть изображение в новом окне Аналогично, мы перечисляем границы в Открытом изображении в новом окне как ( βс , θК, ~с , θК) , Чтобы уменьшить помехи в записи, мы оставим мета-переменную r для пар вида c , l или с , θ , Затем мы вводим связанные переменные переменные vрК описание возможного статического изменения в коде ТА для тактовой частоты βрК и соответственно изменить систему ограничений TDT.
Изменение границ влияет только на ограничения инварианта местоположения. Открыть изображение в новом окне и защитные ограничения перехода. Открыть изображение в новом окне . Таким образом, мы определяем соответствующее инвариантное вариационное ограничение Открытое изображение в новом окне и защищаемое вариационное ограничение Открытое изображение в новом окне, которое фиксирует изменения с привязкой к часам.
Тогда легко понять, что можно выполнить систему таким образом, что это свойство будет нарушено.
Для облегчения локализации неисправностей и отладки таких моделей в процессе проектирования был представлен подход к получению минимального количества ремонтов по параметрам доступности моделей ТА и НТА по времени.
Подход включает формализацию ТДТ с использованием линейной реальной арифметики, ремонтную стратегию, основанную на решении MaxSMT, определение критерия приемлемости и испытания для расчетного ремонта, разработку прототипа инструмента для анализа и ремонта, а также применение предложенного метода к ряду ситуационных исследований реальной сложности. Насколько известно, это первая строгая обработка контрпримеров при проверке моделей в режиме реального времени. Не знаю о каких-либо существующих подходах к ремонту для моделей TA или NTA, и это делает невозможной сравнительную экспериментальную оценку.
Тем не менее, я заметил, что проведенный мной анализ позволяет рассчитать значительное количество допустимых ремонтов в пределах реалистичных расчетных временных рамок и потребления памяти.
Будущие исследования будут посвящены разработке и реализации стратегий ремонта для дальнейших синтаксических особенностей ТА и НТА, включая операторы ложных сравнений в инвариантах и защитных приспособлениях, ошибочные ссылки на переменные часов, излишние или отсутствующие сбросы для часов и неправильный выбор срочного состояния. Кроме того, надо рассмотреть взаимодействие между различными видами ремонта и разработать уточненные стратегии для определения их приемлемости. Наконец, планируется расширить подход, разработанный в данной работе, для определения критериев фактической причинно-следственной связи между временными нарушениями собственности в моделях НТА на основе парадигмы контрфактуального обоснования причинно-следственной связи.