3. Анализ и совершенствование модели ПЛК
В предыдущем разделе была представлена система моделирования ПЛК. Согласно этой стратегии, мы можем абстрагировать систему ПЛК в формальную модель для проверки модели. Таким образом, достоверность этой модели будет напрямую определять результаты проверки модели. Если модель не полностью покрывает исходную систему (мы называем ее меньше исходной системы), это может привести к тому, что некоторые ошибки останутся необнаруженными; если реальная система может полностью покрыть модель, но она содержит много состояний, которых нет у исходной системы (мы называем ее меньше исходной системы), что может внести некоторые ошибки, которые не существуют в реальной системе. Это называется псевдоошибкой. Таким образом, существует две необходимые стратегии моделирования.
Во-первых, чтобы найти все ошибки в системе, необходимо построить достаточно большую модель, чтобы охватить все состояния исходной системы; во-вторых, модель должна быть максимально приближена к реальной системе. Это позволит не только сократить пространство состояний, но и повысить эффективность. Исходя из этих требований, мы проанализируем модель временных интервалов. Предложение 1. Если модель временного интервала соответствует свойствам, то и модель реальной системы ПЛК также соответствует. Правильность Предложения 1 следует из взаимосвязи между двумя моделями. Это означает, что все, что произойдет с реальной моделью, содержится в модели временного интервала, а модель временного интервала больше реальной модели. Если не удастся найти контрпример с помощью модели временных интервалов, то можно доказать правильность реальной модели ПЛК; с другой стороны, если мы найдем контрпример, то не сможем определить, есть ли в реальной системе ПЛК ошибки. Иными словами, обратное утверждение 1 ложно. В этом случае требуется ручное вмешательство для анализа контрпримера, чтобы определить, является ли он надуманной ошибкой.
Стратегия моделирования временных интервалов позволяет получить обобщенную модель ПЛК, и многие исследования, основанные на NuSMV, также используют стратегии, похожие на модель временных интервалов, для моделирования систем ПЛК. Однако "модель временного интервала" значительно отличается от реальной модели и нуждается в улучшении. Это отклонение заключается в том, что "модель временных интервалов" не отражает характеристики высокоскоростного сканирования ПЛК и низкоскоростного сканирования одновременных объектов. То есть все изменения в окружающей среде должны сканироваться высокоскоростным ПЛК, но модель временных интервалов игнорирует высокоскоростные характеристики ПЛК, поэтому изменения во внешней среде могут не сканироваться. В ответ на вышеуказанные проблемы, принимая во внимание физические характеристики внешнего высокоскоростного сканирования и низкоскоростного параллелизма, стратегия моделирования временных интервалов будет улучшена путем добавления механизма ожидания уведомления. Основываясь на модели интервалов, каждый объект одновременного состояния должен быть заблокирован и ждать где-то после завершения передачи данных. Только когда контроллер ПЛК полностью просканирует хотя бы один раз, механизм ожидания уведомления будет работать.
Параллельный объект удаляет блок и продолжает работу. Затем перенос завершается. Процесс завершения переноса параллельным объектом с помощью механизма ожидания уведомления показан на рисунке 2:
t0: Передача начинается, блокируется и уведомляет контроллер ПЛК.
t1-tm: ПЛК полностью сканирует m раз (m в
По крайней мере).
tm 1: Параллельный объект получает уведомление PLC и передача завершается.
Этот механизм гарантирует, что каждое изменение состояния параллельного объекта может быть просканировано контроллером ПЛК хотя бы один раз. Предложение 2 После добавления механизма ожидания уведомления модель становится подмножеством модели временных интервалов.exist
В то же время модель может включать в себя все ситуации реальной модели. Другими словами, если модель добавляет механизм ожидания уведомления, который соответствует атрибутам, то реальная модель системы ПЛК также соответствует им. Использование Предложения 1 для доказательства Предложения 2 аналогично. Из предложения 2 видно, что модель механизма по-прежнему обладает хорошими свойствами после добавления механизма ожидания уведомления. Как уже говорилось, к абстрактным системным моделям предъявляются два требования: во-первых, чтобы реальная система была полностью включена, а во-вторых, чтобы модель была как можно ближе к реальной системе. Первое предложение состоит в том, чтобы доказать, что модель временного интервала включает реальную систему. Если с помощью инструментов проверки моделей доказать, что абстрактная модель удовлетворяет определенным свойствам, то реальные свойства системы также будут этому удовлетворять. Но эта модель не совсем равна реальной модели, она должна быть намного больше реальной модели. По сравнению с моделями временных интервалов, эта модель еще больше сокращает расстояние между реальными системами, значительно уменьшая вероятность обнаружения ложных ошибок.
Инструмент проверки модели выдаст контрпример, нарушающий свойство системы; вручную легко определить, верен ли контрпример в реальной системе или нет. Если ошибка в исходной системе действительно существует, то мы находим контрпример. В противном случае ошибка возникает из-за того, что абстрактная модель больше реальной системы, что является надуманной ошибкой. Таким образом, хотя эта модель временного интервала не является полностью эквивалентной оригинальной системе, с ее помощью мы можем судить о том, удовлетворяет ли система определенному свойству, и если нет, то найти конкретный контрпример (чтобы определить, является ли это псевдоошибкой, необходимо провести дополнительные проверки). Модель не эквивалентна исходной системе главным образом потому, что в реальной системе существует множество факторов, которые трудно смоделировать, и некоторые из них могут приводить к ошибкам. Если бы все факторы были смоделированы, это привело бы к построению огромной модели, которую невозможно проверить или просто реализовать. Модель временных интервалов абстрагирует ключевые факторы от реальной системы и моделирует их, значительно уменьшая пространство состояний и снижая временную сложность. В то же время, благодаря механизму ожидания уведомлений, модель становится ближе к реальной системе, что не только снижает временную сложность, но и уменьшает псевдоошибки, о которых говорилось ранее.
Проверка NuSMV) реализована на созданной выше модели. Мы сформулировали ряд правил преобразования для построения вышеуказанной модели на входном языке SPIN - Promela. Атрибуты системы также должны быть переведены на Promela. SPIN собирает их вместе, а затем выполняет обнаружение. Язык PROMELA - это C-подобный язык, и семантически они похожи. Поэтому мы просто приведем несколько примеров, чтобы показать основные концепции перевода. Подробную информацию о языке PROMELA можно найти на сайте www.spinroot.com. Мы представим три части файла PROMELA в качестве входных данных для SPIN.
1) Код контроллера ПЛК
Контроллер ПЛК состоит из нескольких сетей.
Код для контроллера ПЛК также генерируется из сети. Конечно, перед этим необходимо объявить нужные переменные. Каждая сеть имеет входные и выходные порты, и каждый порт может быть представлен булевым выражением. Мы присваиваем значение выходному порту с помощью логики
Подсчитайте все входные порты. Это перевод
Сетевой метод ПЛК.
