https://www.ccs.neu.edu/home/turon/reagents.pdf Turon, "Reagents: Expressing and Composing Fine-grained Concurrency"

Underlying the shared state/message passing duality is a deeper one: Isolation versus Interaction. Operations on shared state are generally required to be atomic, which means in particular that they are isolated from one another; concurrent shared-state operations appear to be linearizable into a series of nonoverlapping, sequential operations. Synchronous message passing is just the opposite: rather than appearing to not overlap, sends and receives are required to overlap. Fine-grained concurrent operations straddle these two extremes, appearing to be isolated while internally tolerating (or exploiting) interaction.

Хозяйке на заметку: диаграмма методов изготовления чая из https://en.wikipedia.org/wiki/Tea_processing.

Кстати, на днях начну мини-серию постов по формальным методам в ЖД, так что stay tuned!

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.108.573 Katis, Sabadini, Walters, [2002] "Feedback, trace and fixed-point semantics"

> a monoidal category in which the only arrows are identities is, ignoring the arrows, exactly a monoid structure on the objects, whereas a compact closed category with only identity arrows is an Abelian group. The notion of traced monoidal category in this special case turns out to be cancellative monoid.

Евросоюз объявил 2021й годом железных дорог: https://europa.eu/year-of-rail/. При помощи разноцветных постеров еврократы ставят акценты на экологичности поездов и укреплении дружбы народов (она же "трансграничное сотрудничество"), но где-то на третьих-четвертых позициях мелькает и слово safety. Наиболее строгие гарантии безопасности даёт математика, что равносильно использованию формальных методов в инженерии, в частности формальной верификации. Используются ли такие вещи в железнодорожных целях, и если да, то как? Давайте начнём разбираться.

#railway

Что же можно и нужно верифицировать для поездов?

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

Ключевая тема в железнодорожной безопасности это системы railway signalling (по русски СЦБ). Их разделяют на:

* interlocking, т.е. системы управления семафорами и стрелками, назначение которых - исключать конфликтующие маршруты. Как правило, сосредоточены вокруг станций.
* системы безопасности automatic train protection / control (по русски автоблокировки), в основном следящие за скоростью и дистанцией между составами. Действуют на всем протяжении линии.
* высокоуровневые системы automatic train operation (“автоведение”) и automatic train supervision, частично или полностью берущие на себя функции соответственно машиниста и диспетчера.

Важное направление работ - взаимная интеграция этих систем. Так, крупнейшим паневропейским железнодорожным проектом считается ERTMS, который понемногу вводят в ЕС с конца 90х. Он включает в себя СЦБ-подсистему ETCS, цель которой - стандартизировать работу национальных ATP и завершить переход на радио-протоколы. Аналогичным стандартом для метро и электричек является CBTC, внедряемый европейцами по всему миру с середины 80х. Так мы переходим к теме стандартов.

#railway

Пока идёт работа над следующим постом, внес свой скромный вклад в дело победы логики 2.0 - небольшой стикер пак из иллюстраций "дизайнов" людики за авторством Жана-Ива Жирара.

https://www.tgoop.com/addstickers/Desseins

В любом проекте по формальной верификации крайне важна спецификация - ведь корректность доказывают не “вообще” (что невозможно), а именно относительно строго заданной спецификации, как правило, закодированной формулами или “высказываниями” некоторой логики (в случае correct-by-construction программирования их роль играют типы некоторой достаточно мощной системы). Откуда же черпать спецификации для железных дорог?

В западном мире существуют два общепринятых семейства железнодорожных стандартов:

* евросоюзный CENELEC, от фр. Comité Européen de Normalisation ÉLECtrotechnique - на самом деле, как следует из названия, это целый комитет, публикующий сотни и тысячи регламентов на всевозможное электрооборудование; в контексте верификации ЖД нас интересуют стандарты EN50128 и EN50657, где EN это European Norm.
* североамериканский “набор рекомендаций” от AREMA (от American Railway Engineering and Maintenance-of-way Association), плюс военный стандарт для системного ПО MIL-STD-882.

Стандарты 50128 и 50657 регламентируют непосредственно создание и использование ПО для сигнальных систем и подвижных составов соответственно, они входят в более широкое семейство ЖД-стандартов, в частности 50126 (общий стандарт безопасности), 50129/50159 (сигнальные системы), 50155 (подвижные составы) и т.д. Распространяются они на все уровни ПО, потенциально влияющего на безопасность движения - от аппаратных прошивок и ядер ОС до пользовательских интерфейсов.

50128 существует в 2х вариантах: 2001 и 2011, которые совместимы в одну сторону (т.е, 2011 более строгий). Он вводит понятие Safety Integrity Level или SIL - это пронумерованные от 0 до 4 степени требуемой надежности программы. Использование формальных методов “рекомендуется” для уровней 1-2, и “крайне рекомендуется” для 3-4. Разработку предписывается вести по V-образной модели (см. диаграмму ниже).

В отношении формальных методов стандарт рекомендует: использовать их только для критических компонент, строить высокоуровневые иерархические модели, максимально дискретизируя переменные, и делать упор на автоматические доказательства. В качестве примеров ФМ приводятся:

* алгебры процессов CSP и CCS
* интерактивный пруф-ассистент HOL
* языки спецификаций LOTOS, OBJ, "темпоральная логика", VDM, Z-нотация
* B-метод

#railway

Интересно, станет ли модным reversible computing в свете надвигающейся "циркулярной экономики"?

https://www.cs.tau.ac.il/~shanir/progress.pdf Herlihy, Shavit, [2011] "On the nature of progress"

Ранее упоминалось, что упор для железнодорожной верификации делается на автоматизированных методах, что соответствует таким направлениям ФМ, как 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

https://dalila.sip.ucm.es/isr2021/slides/Bruscoli.pdf Bruscoli, [2021] "An Introduction to the Deep Inference Methodology in Proof Theory"

В современной текстовой речи часто в ироническом смысле используются эрративы (нарочитые искажения синтаксиса а-ля "падонкафская речь") и анаколуфы (то же для грамматики, например закосы под "одесситский говор" со всякими "не делайте мне нервы"). Последний приём (также называемый "солецизм") использовался ещё древними греками. Интересно, что у них же было третье понятие для искажений семантики - т.е., ситуаций, ныне описываемые мемами типа "I don't think it means what you think it means" - так вот греки называли это варваризмом.

https://www.connectedpapers.com/

Визуализатор графа связности для научных статей

Написал заметку по статье о верифицированной императивной кодогенерации из полиэдральной модели: https://www.tgoop.com/plcomp/83

https://code.gouv.fr/ поисковик по опенсорсу французских государственных агентств

психиатр: булевалентности не существует, она не может тебе навредить
булевалентность:

Lemma bvalence (a b : bool) : (a <-> b) <-> a == b.
Proof.
case: a; case: b=>//; split=>//.
- by case=>/(_ isT).
by case=>_ /(_ isT).
Qed.

новый зулип по конструктивной математике: https://constructive-maths.zulipchat.com/