Covalue

Ранее упоминалось, что упор для железнодорожной верификации делается на автоматизированных методах, что соответствует таким направлениям ФМ, как model checking и abstract interpetation. Посмотрим по довольно свежей статье-опроснику Beek et al, [2019] "Adopting Formal Methods in an Industrial Setting: The Railways Case", где и как они применяются.

Заметно, что большая часть усилий идёт на верификацию interlocking систем - это объясняется спецификой темы. Как видно уже из названия таких статей, как
Fantechi, Haxthausen, [2018] "Safety Interlocking as a Distributed Mutual Exclusion Problem", проблематику разрешения конфликтующих маршрутов сводят к уже существующим способам верификации многопоточных/распределенных систем. Т.е., рельсы и составы мыслятся как физический эквивалент потоков исполнения, где аналоги thread interference и race condition приводят к весьма печальным и зрелищным последствиям.

Самым же популярным инструментом, точнее семейством инструментов, выглядит уже упоминавшийся B-method - набор языков спецификации и модел-чекеров, разработка которых началась ещё в 80е в Англии и Франции. Из моделей можно экстрагировать код (в основном, кажется на Ada) - этот процесс называют refinement. B-method широко использовался французами в таких проектах как беспилотная 14я ветка парижского метро и автоматизированные шаттлы в аэропорту Шарль де Голь. По итогам проектов сложился некоторый консенсус по поводу надежности B-моделей, благодаря чему их теперь используют как низкоуровневый формализм, в который транслируют другие модели - например, сети Петри в
Sun, [2016] "Model based system engineering for safety of railway critical systems". Используются и другие инструменты проверки моделей, в частности, NuSMV и Promela/SPIN: https://github.com/jankofron/abz18-casestudy-spin.

В отличие от модел-чекинга, часто используемого для работы со спецификациями, абстрактная интерпретация используется для статического анализа кода. Для safety-critical систем таким кодом часто является C, получаемый из более высокоуровневой программы на датафлоу-языке типа Lustre, которая в свою очередь экстрагируется из Simulink-подобных диаграмм. Пример одновременного использования всех этих инструментов вместе с модел-чекингом можно увидеть в Ferrari et al, [2013] "The Metrô Rio case study". Также об этом рассказывает Xavier Leroy в своей наградной лекции 2016 года "In search of software perfection".

#railway

Wikipedia

Model checking

verifying whether a finite-state model meets a given specification

www.tgoop.com/covalue/41

2.9K viewsJun 25, 2021 at 08:15

Ранее упоминалось, что упор для железнодорожной верификации делается на автоматизированных методах, что соответствует таким направлениям ФМ, как model checking и abstract interpetation. Посмотрим по довольно свежей статье-опроснику Beek et al, [2019] "Adopting Formal Methods in an Industrial Setting: The Railways Case", где и как они применяются.

Заметно, что большая часть усилий идёт на верификацию interlocking систем - это объясняется спецификой темы. Как видно уже из названия таких статей, как
Fantechi, Haxthausen, [2018] "Safety Interlocking as a Distributed Mutual Exclusion Problem", проблематику разрешения конфликтующих маршрутов сводят к уже существующим способам верификации многопоточных/распределенных систем. Т.е., рельсы и составы мыслятся как физический эквивалент потоков исполнения, где аналоги thread interference и race condition приводят к весьма печальным и зрелищным последствиям.

Самым же популярным инструментом, точнее семейством инструментов, выглядит уже упоминавшийся B-method - набор языков спецификации и модел-чекеров, разработка которых началась ещё в 80е в Англии и Франции. Из моделей можно экстрагировать код (в основном, кажется на Ada) - этот процесс называют refinement. B-method широко использовался французами в таких проектах как беспилотная 14я ветка парижского метро и автоматизированные шаттлы в аэропорту Шарль де Голь. По итогам проектов сложился некоторый консенсус по поводу надежности B-моделей, благодаря чему их теперь используют как низкоуровневый формализм, в который транслируют другие модели - например, сети Петри в
Sun, [2016] "Model based system engineering for safety of railway critical systems". Используются и другие инструменты проверки моделей, в частности, NuSMV и Promela/SPIN: https://github.com/jankofron/abz18-casestudy-spin.

В отличие от модел-чекинга, часто используемого для работы со спецификациями, абстрактная интерпретация используется для статического анализа кода. Для safety-critical систем таким кодом часто является C, получаемый из более высокоуровневой программы на датафлоу-языке типа Lustre, которая в свою очередь экстрагируется из Simulink-подобных диаграмм. Пример одновременного использования всех этих инструментов вместе с модел-чекингом можно увидеть в Ferrari et al, [2013] "The Metrô Rio case study". Также об этом рассказывает Xavier Leroy в своей наградной лекции 2016 года "In search of software perfection".

#railway

BY Covalue