Maeslantkering, крупнейший штормовой барьер Европы, стал воплощением инженерного мастерства и прогресса в автономных технологиях 90-х годов прошлого века. Его история это путь от идеи к системе, способной самостоятельно принимать решения, защищая Роттердам и его окрестности от разрушительных наводнений. В этой статье вы узнаете, как инженерам удалось создать конструкцию, способную выдержать натиск стихии, как устроены алгоритмы, определяющие момент закрытия стальных ворот размером с Эйфелеву башню, и как проводился аудит софта, от которого зависят жизни тысяч людей.

Штормовой барьер Maeslant
Штормовой барьер Maeslant

В последние годы активно обсуждается роль искусственного интеллекта в принятии решений в критически важных сферах, таких как медицина или правосудие. Однако уже существуют системы, которые давно функционируют автономно, играя ключевую роль в безопасности. Одним из таких примеров является штормовой барьер Maeslant на реке Маас близ Роттердама. Построенный 27 лет назад, он стал не только инженерным чудом, но и одной из первых полностью автономных систем, защищающих население от разрушительных наводнений.

Роттердам — точка на карте гидротехнической революции

Роттердам находится в Нидерландах — стране, значительная часть которой расположена ниже уровня моря. Такой рельеф делает ее одной из самых уязвимых к наводнениям. Географическое положение усугубляется штормами, которые регулярно обрушиваются на прибрежные районы Северной Европы, вызывая разрушения и человеческие жертвы. Эффективная защита от этих угроз — жизненно важная задача для региона.

Всерьез о необходимости построения штормовых барьеров задумались после одной из самых страшных катастроф в истории Нидерландов. В 1953 году шторм разрушил защитные дамбы, затопил обширные территории и унес жизни более 1800 человек. Чтобы не допустить повторения этой трагедии, был создан проект «Дельта» — грандиозная программа по строительству серии гидротехнических сооружений. Штормовой барьер Maeslant, или, как его называют на родине, Maeslantkering — один из его основных элементов. 

Порт Роттердама, 2024 год
Порт Роттердама, 2024 год

От дамб к штормовым барьерам: как люди защищаются от стихии

С древних времен люди искали способы защитить свои поселения от разрушений во время штормов. Все началось со строительства насыпей, валов и дамб из земли, дерева и камня. Их разнообразие было не слишком велико, основные типы можно увидеть ниже.

Типы дамб
Типы дамб

Простые дамбы помогают предотвращать небольшие затопления, но не слишком эффективны против сильных штормов, а они в последние годы происходят все чаще, что видно на графике Атлантических штормов за последние 60 лет.

Атлантические штормы
Атлантические штормы

Морские порты издавна играют ключевую роль в экономике, связывая торговые пути и обеспечивая развитие регионов. В Средние века такие порты, как Венеция и Генуя, были центрами международной торговли, а эпоха Великих географических открытий только увеличила их стратегическое значение. Сегодня около 80% мировой торговли осуществляется морским транспортом.

С развитием технологий появились более сложные решения для защиты территорий от наводнений, которые позволяли не препятствовать работе порта. В первую очередь, речь идет о штормовых барьерах. Они срабатывают только при угрозе наводнения, а в остальное время порт остается открытым для судоходства. Существует разные типы штормовых барьеров. Выбор применяемого барьера зависит от ландшафта, возможного подъема уровня воды и других факторов. Все основные на данный момент виды барьеров показаны на рисунке ниже.

Типы штормовых барьеров
Типы штормовых барьеров

Первый крупный штормовой барьер был построен в Лондоне в 1983 году — барьер Темзы, сооруженный поперек одноименной реки. Предпосылкой для его создания послужило наводнение 1953 года, разговоры о строительстве шли с 1966 года, а само строительство продлилось с 1974 по 1982 годы. Длина барьера составляет около 520 метров, он состоит из 9 бетонных опор и 10 разводных стальных ворот. Когда шторма нет, ворота находятся на дне реки, не мешая судоходству. В случае угрозы наводнения ворота переходят в рабочее положение, поворачиваясь на 90° и образуя сплошную стену, способную перекрыть движение воды вверх по реке. Существующая конструкция способна защитить Лондон от нагонной волны высотой до 7 метров.

Барьер Темзы, защищающий Лондон
Барьер Темзы, защищающий Лондон

Строительство самого знаменитого барьера MOSE (Modulo Sperimentale Elettromeccanico), закрывающего Венецианскую лагуну от моря, было начато в 2003 году. Он состоит из серии поворотных ворот, которые закрываются в случае неблагоприятного прогноза и предотвращают наводнения в Венеции, сохраняя допустимый уровень воды в пределах города. Ворота представляют собой металлические конструкции шириной 20 метров каждые, длиной от 18,5 до 29 метров и толщиной от 3,6 до 5 метров. Его постоянно модернизируют, а первый боевой запуск произошел в 2020 году. 

Барьер MOSE, закрывающий Венецианскую лагуну от моря
Барьер MOSE, закрывающий Венецианскую лагуну от моря

Проект «Дельта»: 9 дамб и 3 штормовых барьера для защиты Роттердама

Возвращаемся в Роттердам. Строительство проекта «Дельта» в Роттердаме началось в 1960, а закончилось только в 1997 году и заняло почти 40 лет. Проект включает в себя 13 ключевых сооружений, среди которых:

  1. 9 дамб-барьеров, перекрывающих протоки и заливаемые территории.

  2. Шлюз для пропуска судов и сброса уровня воды.

  3. Algerakering — первый штормовой барьер в проекте «Дельта», сдан в эксплуатацию в 1958 году. Он конструктивно состоит из двух подвижных шлюзовых ворот, подвешенных между бетонными башнями. Этот барьер закрывается от 4 до 5 раз в год. Ежемесячно с октября по апрель проходят тестовые закрытия.

Штормовой барьер Algera
Штормовой барьер Algera
  1. Oosterscheldekering — 9-километровый штормовой барьер, сдан в эксплуатацию в 1986 году. Первоначально он был спроектирован и частично построен как закрытая дамба, но после протестов общественности на оставшихся четырех километрах были установлены огромные шлюзовые ворота. Плотина управляется вручную, но есть резервная электронная система безопасности, срабатывающая автоматически. С 1986 года барьер полностью закрывался 28 раз.

Штормовой барьер Oosterschelde
Штормовой барьер Oosterschelde
  1. Maeslantkering — уникальный раздвижной барьер, представляющий собой стальные ворота в 22 метра в высоту и 210 метров в длину, сдан в эксплуатацию в 1997 году. Полностью автономный, однако с постоянной командой в 15 человек, которые занимаются его обслуживанием. Закрывался в боевом режиме 2 раза за все время эксплуатации.

Штормовой барьер Maeslant
Штормовой барьер Maeslant

Строительство Maeslantkering — полностью автономного штормового барьера

Строительство Maeslantkering началось в 1991 и завершилось в 1997 году. Изначально для защиты Роттердама планировалось укрепить существующие дамбы на 50 километров вглубь страны, но в 1980-х годах стало ясно, что это займет лет 30 и обойдется слишком дорого. К тому же это требовало перестройки части исторических центров городов за пределами расширенной дамбы.

Расположение штормового барьера Maeslant
Расположение штормового барьера Maeslant

Первоначальный план был отложен, и в конкурсе победил проект более дешевого, но все еще достаточно надежного штормового барьера. Победивший план предусматривал строительство ворот на опорах по 2 берегам реки и обладал значительным преимуществом: строительство и последующую эксплуатацию предполагалось вести в сухих доках на берегу, так что строительство никак не влияло на работу порта.

Двойные ворота барьера напоминают нарисованные крылья. Их закругленные концы служат барьерами, противостоящими штормам Северного моря. Каждая створка, длиной в 240 метров при средней высоте 22 метра и весом в 6 800 тонн, перекрывает половину ширины судоходного канала, соединяющего Роттердам с морем, сходясь с другой точно посередине реки Маас. Устройство конструкции можно увидеть на рисунке ниже.

Устройство штормового барьера Maeslant
Устройство штормового барьера Maeslant

Каждая из арок ворот находится в сухих доках на берегу, выкопанных ниже уровня воды. Отсутствие воды позволяет беспрепятственно проводить обслуживание и ремонты. Каркас створок — это жесткая структура из сваренных стальных труб, которая равномерно передает нагрузку от штормовых волн к шарнирам. Шарниры диаметром 10 метров и весом 600 тонн каждый работают как гигантские суставы, соединяя арки с мощным бетонным основанием общей массой 52 тысячи тонн. 

Устройство шарового шарнира
Устройство шарового шарнира

Пока доки остаются сухими, ворота остаются неподвижными. В случае штормового прогноза доки наполняются водой, пустотелые створки ворот всплывают и после этого можно приступать к закрытию ворот.

Как закрываются ворота размером с Эйфелеву башню?

Первые полчаса закрытия уходят на то, чтобы створки соединились на середине реки. Как только это происходит, открываются клапаны и створки начинают медленно заполняться водой. Еще час уходит на то, чтобы створки заполнились и опустились на бетонную платформу на дне реки. За счет постепенного перекрытия реки, напор воды, который еще проходит внутрь барьера, увеличивается и это позволяет очистить от ила платформу и обеспечить плотное прилегание ворот к ней.

Изначально предполагалось, что Maeslantkering будет закрываться раз в десять лет,  а через 50 лет из-за подъема уровня моря — каждые 5 лет. За первые 10 лет эксплуатации барьер ни разу не закрылся из-за шторма.

Первый тестовый запуск состоялся в сентябре 1997 года, когда пороговые значения уровня воды были специально понижены, чтобы проверить работоспособность барьера. После этого проверки проводятся ежегодно, чтобы убедиться в исправности механических и программных компонентов барьера и их готовности к реальной эксплуатации. Эти плановые проверки становятся развлечением для туристов, совсем как развод мостов в Санкт-Петербурге. 

Наблюдатели на тестовом закрытии Maeslantkering
Наблюдатели на тестовом закрытии Maeslantkering

При прогнозе подъема уровня воды в Роттердаме до 3 метров выше NAP (нормального амстердамского уровня) или в Дордрехте до 2,9 метров выше NAP, система автоматически инициирует процедуру закрытия барьера. Время планового закрытия совпадает со временем, на которое спрогнозировано превышение уровня воды. Что происходит с самим барьером и портом Роттердама в это время?

  1. 20 часов до закрытия. Оперативная группа вызывается в центр управления барьером.

  2. 8 часов до закрытия. Центр управления портом объявляет, что движение судов будет приостановлено.

  3. 4 часа до закрытия. Открываются клапаны в сухих доках и начинается их наполнение водой. Движение по реке останавливается.

  4. 2 часа до закрытия. Движение судов по каналу Ньюве-Ватервег приостанавливается.

  5. Момент закрытия. Ворота приходят в движение и начинают встречное движение над рекой.

  6. 0,5 часа после закрытия. Створы ворот соединены и начинают погружаться на дно реки.

  7. 1,5 часа после закрытия. Погружение закончилось. Барьер полностью закрыт.

В сезон штормов 2007 года, чтобы проверить работоспособность системы в боевых условиях, порог прогнозного подъема воды был снижен с 3 м до 2,6 м. 8 ноября 2007 года на побережье Нидерландов обрушился шторм. Прогноз высоты воды превысил пороговое значение и барьер был закрыт системой управления из-за шторма впервые с момента его строительства. В 22:00 порт закрыл судоходство, процедура закрытия Maeslantkering началась в 23:10 и завершилась в 01:00. Соседние барьеры были тоже закрыты и впервые с начала проекта Дельта все побережье было защищено от наводнения. После прохождения шторма, система вновь открыла ворота 9 ноября около 17:00.

21 декабря 2023 года Maeslantkering был впервые в истории автоматически закрыт со штатным установленным порогом срабатывания в 3 м. По прогнозу уровень воды в Роттердаме должен быть достигнуть критической высоты около 23:30. Порт Роттердама начал сокращать движение в 16:00 и полностью его закрыл около 18:00. Автоматическая процедура закрытия началась в 20:15. На следующий день в 4:45 ворота снова открылись.

Maeslantkering во время шторма Пиа
Maeslantkering во время шторма Пиа

Кто управляет Maeslantkering?

Тщательный анализ показал, что ручное управление барьером ограничит его надежность. Эксперты проекта опирались на данные исследований, показывающие, что человек при принятии решений ошибается в среднем 1 раз из 1000. Система принятия решений называется BOS (Beslis en Ondersteunend Systeem) и была разработана компанией CMG Den Haag B.V. по заказу Rijkswaterstaat (RWS) — Министерства транспорта, общественных работ и водного хозяйства Нидерландов. Проект был завершен в октябре 1998 года в срок и уложившись в запланированный бюджет.

BOS управляет не только барьером Maeslantkering, но и соседним Hartelkering, координируя действия для более эффективной защиты от штормовых приливов. Несмотря на свою автономность, процедура закрытия может быть инициирована вручную.

BOS спроектирован как конструктор, состоящий из самостоятельных подсистем:

  • 2 сменных гидравлических симуляционных модели, основанные на данных о поведении воды. Они позволяют интегрировать данные о климате, гидрологии и инфраструктуре для создания точных симуляций. Обновление моделей происходит ежегодно;

  • скрипт BOS, который содержит в себе правила принятия решений о закрытии Maeslantkering. Он состоит из независимых сценариев, которые можно корректировать без воздействия на другие компоненты;

  • библиотеки для внутреннего и внешнего взаимодействия;

  • графический пользовательский интерфейс.

Для работы скрипта BOS каждые 10 минут собирает метеорологические данные из внешних систем, отслеживает текущее состояние барьера и использует модели имитации наводнений для прогнозирования уровня воды. Основные внешние взаимодействия системы приведены на рисунке ниже.

Внешние взаимодействия системы BOS
Внешние взаимодействия системы BOS

Проектирование автономной системы управления

Автономность Maeslantkering опирается на сложную систему управления BOS, которая объединяет гидравлические модели, алгоритмы принятия решений и визуализацию данных. Чтобы гарантировать надежность и безопасность системы, ее разработка и верификация основывались на строгих стандартах и формальных методах. Одним из ключевых инструментов, использованных для описания и проверки компонентов BOS, стал формальный язык Z, предоставляющий точные средства моделирования распределенных систем и анализа их корректности.

В проекте BOS на различных этапах процесса разработки использовались разные формальные методы. Отправным шагом стала функциональная спецификация (FS) — комбинации требований, дополненных решениями по реализации и описаниями алгоритмов. Она представляла собой документ на естественном языке, дополненный диаграммами потоков данных, объемом около 700 страниц.

В проекте было принято решение не формализовывать спецификацию, а начать формализацию на уровне технического дизайна, который разрабатывался на основе спецификации. Структура управления была описана на языке Promela; структуры данных и операции были описаны с использованием формального языка Z. Итоговый набор формальных методов, примененных к каждой подсистеме, представлен на диаграмме ниже.

Использование формальных языков в компонентах системы
Использование формальных языков в компонентах системы
  1. Ключевые подсистемы:

  • PS: Интерпретатор скриптов, выполняющий скрипт принятия решения

  • SBI: Интерфейс для гидравлической модели

  • CCL: Библиотека для коммуникаций и утилит

  • IBS: Запуск, остановка, мониторинг и управление другими подсистемами, а также обработка ошибок и их устранение

  1. Критически важные подсистемы:

  • INW: Сбор метеорологических данных

  • KER: Управление аппаратным обеспечением барьера

  • OPR: Связь через факс, семафор и терминал

  1. Некритические подсистемы:

  • GUI: Пользовательский интерфейс системы BOS

  • RAP: Генерация отчетов после управления барьером

  • DBE: Архивирование данных, полученных во время работы системы, и их последующая очистка

Формальный язык Z в двух словах

Как и в любом масштабном инженерном проекте, где ставки невероятно высоки, скучная математика и бездушная логика оказались незаменимыми. Для управления такой сложной системой, как BOS, потребовались инструменты, которые исключают двусмысленность и позволяют проверить каждую деталь. Здесь на сцену выходит формальный язык Z — незаметный герой, который превратил строгие математические модели в основу надежности барьера Maeslantkering.

Z основан на теории множеств и предикатной логике. Спецификация на Z делится на компоненты, называемые схемами, которые описывают как динамические, так и статические аспекты системы. 

  • Динамические аспекты включают переходы между состояниями.

  • Статические аспекты включают допустимые достижимые состояния и инварианты, которые должны сохраняться при переходах.

Схемы записывается в прямоугольной рамке, где верхняя часть описывает переменные, а нижняя — ограничения или условия. 

Типовая Z-схема
Типовая Z-схема

На рисунке выше символ Ξ указывает, что в заданной операции состояние буфера не изменяется. Знак вопроса у переменной input? типа inputType обозначает, что это входная переменная, тогда как восклицательный знак у переменной output! типа outputType обозначает выходную переменную.

Давайте рассмотрим Z-схему, описывающая два целых числа x и y, связанных условием x меньше y.

State

x, y: ℤ

x < y

В Z нотации используются следующие типы данных:

  • Множества: {1, 2, 3}, ℕ (натуральные числа), (целые числа).

  • Последовательности: seq X — последовательность элементов типа X.

  • Функции: A → B — отображение множества A в множество B.

Также существует набор операторов, позволяющих описывать взаимосвязи:

  • Логические: (и), (или), ¬ (не), (импликация).

  • Теория множеств:

    • (объединение), (пересечение).

    • (принадлежность), (не принадлежит).

  • Кванторы:

    • ∀ x ∈ A • P(x) — для всех x из A выполняется P(x).

    • ∃ x ∈ A • P(x) — существует x в A, для которого выполняется P(x).

  • Функции:

    • f(x) — применение функции f к аргументу x.

    • dom f — область определения функции f.

    • ran f — множество значений функции f.

Пример использования Z-спецификации в BOS

Рассмотрим функцию определения избыточного уровня воды (DEW),  являющуюся одной из функций, отвечающих за принятие решений. 

Что нам важно про нее знать?

  1. DEW Использует прогнозы уровня воды от системы SOBEK для трех городов: Роттердам, Дордрехт и Спейкениссе.

  2. Анализирует прогнозы на 24 часа с шагом 10 минут.

  3. Учитывает критическое превышение — ситуацию, когда уровень воды остается повышенным спустя 20 минут.

  4. Работает с неопределенными значениями, что отражается в типах данных и логике обработки.

Главная Z-схема в компоненте DEW описывает общую структуру и последовательность выполнения операций для определения критического превышения уровня воды. Она представлена следующим образом:

DEW == SetEvaluationParams >> DetModelEvaluation >> (EvaluationFailed ∨ CoreDEW)

Что это значит? Шаг SetEvaluationParams отвечает за обработку входных параметров, которые поступают в компонент DEW из скрипта. Эти параметры включают:

  • Максимальные допустимые уровни воды для каждой локации.

  • Интервал времени, в котором должны оцениваться прогнозы.

На выходе SetEvaluationParams преобразует входные данные в удобный формат для дальнейшей обработки. Шаг DetModelEvaluation взаимодействует с гидравлическим эмулятором, который предоставляет прогнозы уровня воды. Работает по следующей логике:

  • Проверяет наличие прогноза в базе данных.

  • Если прогноз найден и актуален, он используется.

  • Если прогноза нет, эмулятор (SOBEK) запускает новый расчет, и результат сохраняется в базе данных.

Дальше происходит разветвление логики: (EvaluationFailed ∨ CoreDEW). Если предыдущий шаг не удается (например, данные недоступны или прогнозы не рассчитаны), система переходит к EvaluationFailed. Если данные прогноза получены, следующим шагом идет CoreDEW — основной этап, где происходит поиск критических превышений уровня воды в прогнозах. Он состоит из следующих действий:

  • Проверяется, превышает ли уровень воды пороговое значение в момент времени.

  • Анализируется, сохраняется ли превышение через 20 минут (условие критического превышения).

  • Если критическое превышение найдено, система устанавливает флаг Excess и фиксирует время события ExpTime.

Теперь давайте посмотрим на пример Z-спецификации для критического превышения в компоненте DEW описывает, как система определяет критические ситуации на основе прогнозов уровня воды:

let ExcessTimes ==

{s : LocSeqs; l : dom LocList; i : N |

    i ∈ 1..(#s.vals) − 2 ∧

    s.loc = l ∧ (s.vals i).val > (LocList l) ∧

    (s.vals (i + 2)).val ≥ (s.vals i).val} ∩ Interval

Давайте разбираться в деталях:

s : LocSeqs

LocSeqs — это таблица прогнозов для каждой локации, где каждая запись (s) содержит:

  • Локацию (s.loc), например, Роттердам или Дордрехт.

  • vals — последовательность значений уровня воды во времени.

  • Начальную точку прогноза (TBegin).

l : dom LocList

LocList связывает локацию (например, Роттердам, Дордрехт или Спейкениссе) с ее максимальным допустимым уровнем воды. dom LocList — множество всех локаций, для которых определены максимальные уровни воды.

i ∈ 1..(#s.vals) − 2

Цикл проходит по индексам значений прогноза (s.vals) до предпоследнего значения. Поскольку условие критического превышения требует проверки значений через 20 минут, используется i + 2.

s.vals i.val > (LocList l)

Проверяется, что текущее значение уровня воды s.vals i превышает максимальный уровень для локации LocList l

(s.vals (i + 2)).val ≥ (s.vals i).val

Через 20 минут (следующий индекс i + 2) уровень воды остается не ниже текущего (), что подтверждает критическое превышение.

Interval

Результаты ограничиваются интервалом оценки, заданным скриптом. Только значения, попадающие в этот интервал, учитываются. Формула определяет множество временных точек ExcessTimes, где:

  • Прогноз показывает превышение уровня воды.

  • Через 20 минут уровень остается стабильно высоким.

  • Временная точка попадает в интервал оценки.

Если множество ExcessTimes не пустое, значит, обнаружено критическое превышение.

Формальные методы в действии

Создание и особенно запуск системы управления уровня Maeslantkering невозможно без тщательной проверки каждого элемента. После того как формальные методы и язык Z помогли задать строгие правила для системы BOS, следующим шагом стало их применение в реальной разработке и тестировании. Процесс верификации включал в себя следующие шаги:

  1. Анализ коммуникационных протоколов

Применялся на этапе проектирования и интеграции системы. Протоколы взаимодействия между BOS и внешними системами моделировались с использованием языка Promela и проверялись в среде SPIN, чтобы устранить возможные ошибки в коммуникациях еще до начала программирования.

Результат: обнаружены фатальные ошибки в изначальной реализации протоколов, которые могли привести к сбоям в коммуникации, но были устранены.

  1. Проверка формальных спецификаций на Z

Выполнялась после завершения этапа технического проектирования. Это включало анализ корректности предусловий, постусловий и инвариантов для критически важных подсистем, таких как PSI (интерпретатор скриптов) и KER (управление аппаратным обеспечением).

Результат: выявлено множество неоднозначностей и неполноты в исходной функциональной спецификации, которые были устранены на этапе разработки технического дизайна (TD).

  1. Ручное доказательство полноты схем операций

Использовалось в процессе реализации, чтобы убедиться, что разработанные на языке Z схемы операций охватывают все возможные комбинации входных данных и состояний. Этот шаг был особо важен для ключевых подсистем, включая INW (сбор данных) и SBI (взаимодействие с гидравлическими моделями).

  1. Сравнение спецификаций и кода

Проводилось на этапе тестирования и отладки системы. Реализованные на C++ компоненты сравнивались с формальными требованиями, чтобы убедиться в их соответствии исходным спецификациям.

  1. Верификация кода на C++

Выполнялась на финальных этапах разработки. Код проверялся на предмет критических ошибок, таких как упущения в логике циклов или некорректная обработка данных, выявленных в процессе тестирования и анализа.

Пример верификация кода на C++ в BOS

Вернемся к функции определения избыточного уровня воды (DEW). Основная задача кода — поиск критического превышения уровня воды на основе данных прогнозов, предоставленных системой SOBEK. Давайте посмотрим на основной фрагмент кода:

for (int item = 0; !ExpTime.IsDetermined() && (item < s.GetSize() - 2); ++item) {

    if (TLoop >= TBegin && TLoop <= TEnd) {

        const int next_wl = s.vals.ElementAt(item).val;

        if (next_wl > MaxLevel) {

            Excess = TRUE;

            // Проверка на критическое превышение

            if (s.vals.ElementAt(item + 2).val >= next_wl)

                ExpTime.Set(TLoop);

        }

    }

    TLoop += stepsize;

}

Цикл for перебирает прогнозы уровня воды для каждой локации, начиная с первого элемента (item = 0). В коде приведено 2 условие выхода из цикла:

  • !ExpTime.IsDetermined(): время критического превышения еще не зафиксировано.

  • item < s.GetSize() - 2: цикл не выходит за пределы массива данных прогноза.

Проверка интервала оценки реализована через if (TLoop >= TBegin && TLoop <= TEnd), где TLoop — текущий момент времени прогноза, а TBegin и TEnd — границы интервала оценки, которые поступают в DEW как параметры.

Для определения превышения прогнозного уровня воды порогового значения используется следующий код:

const int next_wl = s.vals.ElementAt(item).val;

if (next_wl > MaxLevel)

Где next_wl: текущий прогноз уровня воды из последовательности s.vals, а MaxLevel: максимальный допустимый уровень воды для локации.

Для проверки на критическое превышение используется код

if (s.vals.ElementAt(item + 2).val >= next_wl)

    ExpTime.Set(TLoop);

Условие критического превышения: через 20 минут (элемент item + 2) уровень воды остается не ниже текущего. ExpTime.Set(TLoop): фиксируется время TLoop, если было обнаружено критическое превышение. 

Значение времени увеличивается на шаг stepsize, соответствующий интервалу между прогнозами (например, 10 минут). Использование неопределенных значений (ExpTime.IsDetermined()) позволяет коду работать с ситуациями, когда данные отсутствуют. 

Код на C++ напрямую реализует логику Z-спецификации для поиска критических превышений. Например:

  • Условие next_wl > MaxLevel соответствует проверке превышения уровня воды.

  • Условие s.vals(item + 2).val >= next_wl отражает требование «через 20 минут уровень остается высоким».

В результате верификации были найдены ошибки и в Z-спецификации, и в коде. В Z-спецификации не учитывался интервал оценки, который присутствовал в реализации на C++. В коде же были найдены следующие ошибки:

  • Последние два элемента массива прогнозов не анализировались из-за условий цикла.

  • В базе данных прогнозов могло быть несколько значений для одной локации; код допускал только одно значение.

Maeslantkering: 27 лет без критических сбоев

Maeslantkering это не только инженерное чудо, но и доказательство того, как продуманное проектирование и строгие стандарты могут обеспечить десятилетия стабильной работы. За 27 лет эксплуатации на этом гигантском штормовом барьере не произошло ни одного критического сбоя. Однако даже за такой впечатляющей статистикой стоят регулярное обслуживание, тестирование и множество уроков, полученных за годы эксплуатации. Что же позволило Maeslantkering стать символом надежности на этапах после проектирования?

  1. Строгий контроль состояния всех систем 

Все инциденты записываются и отправляются инженеру, даже если кто-то просто споткнулся о провод и он вылетел. При этом:

  • незначительные инциденты есть всегда;

  • большинство инцидентов возникает между 9:00 и 17:00;

  • инциденты почти никогда не возникают между Новым годом и Рождеством.

  1. Обслуживающая команда автономного барьера

В команду обслуживания Maeslantkering входят инженеры-механики, электроинженеры, программисты, ИТ специалисты, гидрологи и метеорологи. Все они обеспечивают бесперебойную работу барьера, проводят регулярные проверки и выполняют необходимое техническое обслуживание, чтобы барьер был готов к работе в любой момент. При проектировании было определено 9 000 возможных сценариев отказов и для каждого сценария определен порядок действий и сформировано 210 рабочих групп для устранения неполадок, исходя из необходимой экспертизы.

Объем человеческого вмешательства был сильно недооценен при проектировке и строительстве системы. Оно требуется постоянно, то для ремонта насосов или клапанов, то для подключения отвалившихся кабелей. 

  1. Строгий контроль изменений и жесткие ограничения для цикла разработки

Релиз BOS обновляется всего раз в год, в сезон штормов с октября по апрель не вносятся никакие изменения. Ключевым элементом приемочного тестирования является использование данных 20 реальных исторических штормов. Такой подход позволяет оценить процесс принятия решений и реакцию системы в условиях, максимально приближенных к реальным. Моделирование этих штормов занимает около 60 дней.

Релиз должен быть готов к тестированию в июне, иначе приемочные испытания не успеют пройти к дате итоговых испытаний, которые планируются на год вперед. А запросы на изменения, цикл разработки которых не укладывается в сроки одного года, обычно считаются «невыполнимыми». 

Будущее автономных систем

Автономная система BOS, управляющая Maeslantkering, была разработана с высочайшим уровнем ответственности, точности и надежности. Она доказала, что решения, которые когда-то казались прерогативой человека, могут быть переданы алгоритмам — при условии строгой верификации и соблюдения стандартов разработки.

Сегодня, когда активно ведутся дискуссии о том, стоит ли позволять ИИ принимать самостоятельные решения в критических отраслях, пример Maeslantkering показывает: в контролируемых условиях технологии способны не только поддерживать человека, но и полностью брать на себя ответственность в моменты, когда ставка — тысячи жизней и миллиарды евро.

В то время как BOS принимает решения полностью автономно, а искусственный интеллект думают запрещать в отдельных отраслях, все популярнее становятся полуавтоматические системы — системы поддержки принятия решений. Они делают выводы с учетом растущего числа неопределенностей и дают прогнозы на период от года до десятков лет. Впрочем, ответственность за принятие решения все равно остается на человеке.

Комментарии (10)


  1. achekalin
    31.07.2025 06:18

    Но почему он назван крупнейшим? Я таковым привык считать дамбу в Питере, и, стоит по ней прокатиться, начинаешь верить в этоточень легко.

    Кстати, подобные "ворота" там тоже есть.


    1. vater_nicht
      31.07.2025 06:18

      Ворота в статье - побольше будут и построены раньше. Но точно не "размером с Эйфелеву башню". Если только не сравнивать вес.


      1. Shaman_RSHU
        31.07.2025 06:18

        Ворота в статье будут побольше в надводной части, не весь комплекс. Застал, когда их строили, к сожалению не нашел в открытом доступе фотографий строительства.



  1. aik
    31.07.2025 06:18

    В какой момент скрипт вида "если <такие-то условия> то закрой ворота" превращается в ИИ?

    инциденты почти никогда не возникают между Новым годом и Рождеством.

    Между каким именно Рождеством? Страна католическая, то есть между 1 января и 25 декабря инцидентов нет? То есть все случаются между 25 декабря и 1 января?


    1. ssj100
      31.07.2025 06:18

      Ну ясно что автор сделал локализацию... c 1 января по 7 скорее там меньше народу и меньше инцедентов


      1. aik
        31.07.2025 06:18

        Тогда возникает вопрос в том, почему именно с 1 по 7? Ибо это в европах уже вполне рабочая неделя, на неё выходные со всего года никто не переносит. :)


        1. ssj100
          31.07.2025 06:18

          Отходят от новогодних праздников и не устали и сконцентрированы на работе


  1. lleo_aha
    31.07.2025 06:18

    Вот что самое для меня загадочное - без экзотических Z и Promela (надеюсь это теоретические языки, а то ещё могут быть баги в компиляторах/интерпретаторах) прям вот никак нельзя было строго формализованную проверку выполнить?

    Тем более что приемочные тесты все равно на реальных исторических данных, в итоге...


  1. nerudo
    31.07.2025 06:18

    На чем, интересно, работает эта BOS? Вот будет забавно, если какое-нибудь Win 3.1 или OS/2 Warp3.