Formal Methods in Safety-Critical Railway Systems

Thierry Lecomte, Thierry Servat, Guilhem Pouzancre. ClearSy, Aix en Provence, France. In: SBMF 2007 (2007)

В этой статье представлены несколько последних применений B-метода к критичным по безопасности системам, а конкретно - к контроллерам раздвижных дверей на платформах. Функциональная спецификация этих систем, основана на формальной модели, для которой была доказана правильность работы при условии корректной работы отдельных ее компонент.

B-метод был создан в конце 80х для разработки критичного по надежности программного обеспечения и был успешно применен в индустрии транспорта. Первое успешное применение в реальных условиях было в Парижском метро - были написаны 110000 строк B-моделей и в сгенерированном по ним коде не было найдено ни одной ни одной ошибки после многочисленных проверок.

В середине 90х появились полее широкие возможности использования B. Стало возможно применять его не только для разработки программного обеспечения, но и для проектирования и анализа целых систем. Для этого B был расширен до Event-B, в который добавили возможность работы и с аппаратным оборудованием.

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

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

Для каждой модели отдельно проверяется внутренняя корректность каждой отдельной модели и соответствие ее абстракции, а так же то, что каждое изменение не противоречит абстракции.

А после этого для всего набора моделей вместе доказывается корректность, при этом для каждой внутренней модели рассматривается ее абстракция, а не полная модель.

Двери на платформах нужны в первую очередь для обеспечения безопасности пасажиров. На ClearSy стояла задача за 10 месяцев разработать контролер, который будет определять прибытие, стоянку и отбытие поезда без прямого контакта с ним. А во время стоянки контролер должен следить за открытием и закрытием дверей поезда и управлять платформенными дверьми в соответствие этим. При этом контролер должен быть SIL3-совместимым (вероятность ошибки системы меньше 10^-7)

Для достижения требуемого уровня безопасности, разработчики решили использовать метод, во многом основанный на формальном B-методе и применили его на большей части стадий проекта.

До начала разработки был проведен функциональный анализ системы для оценки полноты и поиска неоднозначностей в поведении. B-метод использовался для

• Проверки на целостной системе (контроллер + двери) того, что все функциональные ограничения и требования безопасности выполняются.
• Наблюдения за опасным поведением системы

Уже на основе этого анализа удалось отказаться от первого варианта решения задачи, т.к. стало понятно, что добиться требуемого уровня точности за столь короткий срок не удастся.

Для второго варианта решения на основе инфракрасных, ультразвуковых и лазерных сенсоров. Для этого решения были написаны B-модели, которые учитывали только нормальное поведение сенсоров. Модели из предыдущего шага были использованы без каких-либо изменений. Это очень важно, т.к. без дополнительной разработки удалось проверить новый вариант решения.

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

Для каждой стадии и всех вариантов ошибок сенсоров были вычислены вероятности и в дальнейшем проверены в ходе 8-месячного эксперимента. С учетом этих вероятностей модели были модифицированы для достижения требуемого уровня точности.

Итоговые модели были анимированы с помощью http://www.brama.fr для проверки того, что для всех сценариев поведение соответствовало ожиданиям. Эта анимация не была часть проверки, а просто помогла разработчикам сопоставить модели с реальностью.

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

Стояла задача разаботки SIL3-совместимой системы управления платформенными дверьми за 10 месяцев.

Разработка с помощью B-метода позволила прозрачно опробовать несколько вариантов детектирования событий и проверки их с помощью одной функцинальной модели.

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

За 8 месяцев работы система обработала примерно 96000 поездов, при этом в работе не было зафиксировано ни одной ошибки.

1. http://www.brama.fr