Differences

This shows you the differences between two versions of the page.

--- mdd:formal_methods_in_safety_critical_railway [2014/06/03 06:22] – tolmalev
+++ mdd:formal_methods_in_safety_critical_railway [2026/08/29 07:59] (current) – external edit 127.0.0.1
@@ Line 1: / Line 1: @@
+====== 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/|http://www.brama.fr]] для проверки того, что для всех сценариев поведение соответствовало ожиданиям. Эта анимация не была часть проверки, а просто помогла разработчикам сопоставить модели с реальностью.
+После этого по проверенным моделям был сгенерирован исходный код, для которого уже не нужны юнит-тесты, т.к. эта часть тестирования покрывается проверкой исходных моделей.
+===== Заключение =====
+Стояла задача разаботки SIL3-совместимой системы управления платформенными дверьми за 10 месяцев.
+Разработка с помощью B-метода позволила прозрачно опробовать несколько вариантов детектирования событий и проверки их с помощью одной функцинальной модели.
+По итоговым моделям был сгенерирован 100%-протестированный исходный код, без ошибок (соответствующий спецификации).
+За 8 месяцев работы система обработала примерно 96000 поездов, при этом в работе не было зафиксировано ни одной ошибки.
+===== Ссылки =====
+  - [[http://www.brama.fr/|http://www.brama.fr]]