АльтаРика
Парадигма | Объектно-ориентированный, прототипно-ориентированный |
---|---|
Разработчик | Ассоциация Алтарика |
Впервые появился | 1998 |
Стабильная версия | 3.0
/ 3.0 (2020) |
ТЫ | Кросс-платформенный |
Лицензия | Собственное программное обеспечение |
Расширения имен файлов | .все |
Веб-сайт | www |
Основные реализации | |
Сесилия ОКАС, проектировщик по безопасности, SIMFIA, мастер AltaRica | |
Под влиянием | |
Lustre7, Модельика |
AltaRica — это объектно-ориентированный язык моделирования, предназначенный для вероятностного анализа рисков и безопасности. Это представитель так называемого модельного подхода в проектировании надежности . Начиная с версии 3.0, он разрабатывается некоммерческой ассоциацией AltaRica, которая совместно разрабатывает связанную среду моделирования AltaRica Wizard.
История [ править ]
Проектирование AltaRica началось в конце девяностых годов на факультете информатики Университета Бордо (LaBRI). Обоснованием создания нового языка моделирования было преодоление трудностей, с которыми сталкиваются аналитики безопасности (в авионике, атомной, автомобильной и нефтегазовой промышленности) при использовании «классических» формализмов моделирования, таких как деревья отказов , цепи Маркова или стохастические сети Петри . Этим формализмам на самом деле не хватает ни выразительной силы, ни структурирующих конструкций, ни того и другого. Первые научные статьи. [1] [2] [3] [4] о языке были опубликованы с 1998 по 2008 год. [5] [6] [7] Первоначальная версия языка опиралась на три технологии: автоматы с конечным числом состояний , которые тщательно изучались командой LaBRI, работающие над формальными методами верификации программного обеспечения, [8] структурированное программирование, вдохновленное языком моделирования Lustre , и программирование в ограничениях. [9] Эта последняя технология, хотя и элегантная и мощная, на практике оказалась неэффективной. Разрешение ограничений было слишком затратным с точки зрения вычислений, чтобы масштабировать его на системах промышленного размера. Однако команда LaBRI продолжала работать над этой оригинальной версией, в основном в образовательных целях, улучшая инструменты с годами. [10] [11] [12] [13] Поэтому был сделан первый поворот в разработке версии языка для потоков данных. [14] [15] В потоке данных AltaRica переменные обновляются путем распространения значений в фиксированном порядке. Этот порядок определяется во время компиляции на основе аннотаций, приведенных в модели. AltaRica Data-Flow вызвала значительный академический и промышленный интерес. Для языка были разработаны интегрированные среды моделирования: Cecilia OCAS от Dassault Aviation , Simfia v2 от Airbus -Apsys и Safety Designer от Dassault Systèmes (последний инструмент изначально был клоном Cecilia OCAS, но впоследствии развивался отдельно). Реализовано успешное промышленное применение. [16] [17] [18] [19] Например, AltaRica Data-Flow использовалась для сертификации системы управления полетом самолета Falcon 7X (Dassault Aviation). Ряд кандидатских диссертаций также был посвящен языку и его использованию в различных контекстах. [20] [21] [22] [23] [24] [25] [26] [27] Одним словом, AltaRica Data-Flow достигла научного и промышленного уровня. [28] зрелость. Он до сих пор ежедневно используется для самых разных целей.
Однако опыт показал, что AltaRica Data-Flow можно улучшить несколькими способами, что оправдывает серьезную переработку языка. Эта переработка в конечном итоге привела к появлению AltaRica 3.0. [29] [30] который улучшает поток данных AltaRica в нескольких направлениях. Синтаксис AltaRica 3.0 ближе к Modelica, чем к потоку данных AltaRica, что позволяет облегчить связь между мультифизическим моделированием и симуляцией, а также вероятностным анализом рисков и безопасности. Объектно-ориентированные и прототипно-ориентированные конструкции структурирования были собраны таким образом, чтобы дать языку универсальный и последовательный набор структурирующих конструкций посредством S2ML (язык моделирования структуры системы), который, вероятно, является наиболее полным из всех существующих языков поведенческого моделирования. Кроме того, семантика AltaRica 3.0 была усилена посредством GTS (для систем защищенного перехода), что открывает новые возможности с точки зрения оценки моделей.
Системы охраняемых переходов [ править ]
Системы защищенных переходов принадлежат к семейству математических моделей вычислений, объединенных общим термином (стохастические) конечные автоматы или (стохастические) конечные автоматы. Они были представлены в 2008 году. [31] и позже усовершенствованный [32]
Чтобы проиллюстрировать идеи, лежащие в основе систем защищенного перехода, рассмотрим мотопомпу, которая обычно находится в режиме ожидания, которую можно запускать по требованию и останавливать, когда потребности больше нет. Предположим, кроме того, что этот насос может выйти из строя в работе с определенной интенсивностью отказов λ и что он также может выйти из строя по требованию с определенной вероятностью γ . Наконец, предположим, что насос можно отремонтировать с определенным средним временем ремонта τ .
Затем мы можем представить поведение этого насоса с помощью (стохастического) конечного автомата, изображенного ниже.
Снаружи мотопомпу можно рассматривать как черный ящик с входным потоком жидкости «вход», входным потоком информации «спрос» и выходным потоком жидкости «наружу», т.е. как передаточную функцию, задающую значения «Вход» и «Спрос» вычисляет значение «выход». В рамках исследований надежности поведение систем должно быть абстрагировано, чтобы избежать комбинаторного взрыва ситуаций, на которые следует обратить внимание. Таким образом, потоки обычно абстрагируются как логические значения, true интерпретируется как наличие потока, а false — как его отсутствие.
Уравнение, связывающее «вход» и «требование» с «выходом», не может быть записано напрямую, поскольку моторный насос имеет внутреннее состояние. А именно, можно считать, что насос может находиться в трёх состояниях: «ОЖИДАНИЕ», «РАБОТАЮЩИЙ» или «НЕИСПРАВНЫЙ». На рисунке выше состояния представлены в виде скругленного прямоугольника. Выходной поток «на выходе» принимает значение «истина» тогда и только тогда, когда насос работает, а входной поток «на выходе» имеет значение «истина» (отсюда уравнение в правой части рисунка выше).
Фундаментальная абстракция конечных автоматов состоит в том, что изучаемая система может изменить состояние только при возникновении события. Между двумя событиями ничего не меняется. Возникновение событий описывается посредством переходов, представленных на рисунке стрелками. В системах с защищенными переходами переход помечается событием, имеет определенное предварительное условие, называемое защитой перехода, и определенный эффект, называемый действием перехода. Например, событие «отказ» может произойти только в состоянии «РАБОТА». Его эффект состоит в том, чтобы заставить насос перейти из состояния «РАБОТАЮЩИЙ» в состояние «ОШИБКА». Событие «пуск» может произойти, если насос находится в состоянии «ОЖИДАНИЕ» и если входной расход «запрос» соответствует действительности. Его эффект заключается в переводе насоса из состояния «ОЖИДАНИЕ» в состояние «РАБОТА». И так далее.
Теперь некоторые изменения состояний могут потребовать времени, а некоторые другие произойдут, как только они станут возможными. Например, отказ происходит через определенное время, а насос запускается при необходимости (по крайней мере, на уровне абстракции моделей надежности). Системы защищенных переходов связывают задержки с событиями и, следовательно, с переходами. Эти задержки могут быть либо детерминированными для события «начало», либо стохастическими для события «сбой». На рисунке детерминированные задержки представлены пунктирными стрелками, а стохастические — простыми стрелками.
Наконец, переходы могут конкурировать в одном состоянии. Например, переход «стоп» конкурирует с переходом «сбой» в состоянии «РАБОТА». Однако эта конкуренция не является реальной, поскольку переход «стоп» немедленно запускается (выполняется), когда «спрос» входного потока перестает быть истинным. Настоящая конкуренция происходит между переходами «старт» и «отказ по требованию» в состоянии «ОЖИДАНИЕ». Оба запускаются немедленно, когда входной поток «спрос» становится истинным. В системах защищенных переходов можно связать вероятность возникновения каждого конкурирующего перехода, а именно γ с «failureOnDemand» и для «начать» в нашем примере.
В конце концов, код AltaRica для системы защищенных переходов, который мы набросали, показан на рисунке ниже. Мотопомпа представлена в виде «блока», т.е. контейнера для основных элементов. Блок объявляет четыре переменные: переменную состояния «_state», которая принимает свое значение в домене (наборе символических констант) «MotorPumpState», и три логические переменные потока «demand», «in» и «out». Изначально «_state» принимает значение «STANDBY». Передаточная функция представлена посредством утверждения. Утверждения сообщают, как вычислить значения переменных выходного потока на основе значений переменных входного потока и значений переменных состояния.
domain MotorPumpState {STANDBY, WORKING, FAILED}
block MotorPump
MotorPumpState _state (init = STANDBY);
Boolean demand, in, out (reset = false);
event start (delay = Dirac(0), expectation=gamma);
event failureOnDemand (delay = Dirac(0), expectation=1-gamma);
event stop (delay = Dirac(0));
event failure (delay = exponential(lambda));
event repair (delay = exponential(1/tau));
parameter Real lambda = 1.0e-4;
parameter Real tau = 8;
parameter Real gamma = 0.02;
transition
start: demand and _state==STANDBY -> _state := WORKING;
failureOnDemand: demand and _state==STANDBY -> _state := FAILED;
stop: not demand and _state==WORKING -> _state := STANDBY;
failure: _state==WORKING -> _state := FAILED;
repair: _state==FAILED -> _state := STANDBY;
assertion
out := in and _state==WORKING;
end
Блок «MotorPump» объявляет также пять событий и столько же переходов. Защитники переходов — это логические условия для переменных состояния и потока. Действия переходов изменяют значения переменных состояния. События связаны с задержками и, возможно, ожиданиями (которые используются для расчета вероятностей возникновения переходов в соревновании). Описание как задержек, так и ожиданий может включать параметры.
системы Язык моделирования структуры
В целом, исследуемые системы не состоят из одних простых компонентов, как вышеупомянутый насос с электроприводом. Скорее, они состоят из сети таких компонентов, которые взаимодействуют организованно иерархически.
Чтобы отразить архитектуру системы в модели, нужны специальные конструкции. Именно здесь в игру вступает S2ML (язык моделирования структуры системы). S2ML впервые появился как набор структурных конструкций для AltaRica 3.0. Потом его изучали самостоятельно. [33] [34] На сегодняшний день S2ML последовательно объединяет универсальный набор структурирующих конструкций, возникших в результате объектно-ориентированного и прототипно-ориентированного программирования. [35] [36]
S2ML состоит из ключевых понятий высоты: понятий порта, соединения, контейнера, прототипа, класса, клонирования, создания экземпляра, наследования и агрегации.
- Порты
- Это базовые элементы моделирования, такие как домены, переменные состояния и потока, события и параметры.
- Соединения
- Это отношения между портами, такие как определения доменов, распределения вероятностей, связанные с переменными состояния, определения параметров, переходов и утверждений.
- Контейнеры
- Они собирают объявления портов и соединений, а также других контейнеров, образующих вложенные иерархии. Таким контейнером является блок, описывающий мотопомпу.
- Прототип и клонирование
- Прототипы — это отдельные контейнеры. В АльтаРике блоки — это прототипы. Когда изучаемая система содержит две или более одинаковых частей, дублирование кода было бы утомительным и чревато ошибками. Клонирование дает решение этой проблемы: первая часть описывается, затем остальные просто получаются путем клонирования первой. Обозначение через точку позволяет получить доступ к портам, объявленным во вложенных блоках, как показано утверждением в приведенном выше коде.
block System
// ...
block Line1
// description of line 1
end
clones Line1 as Line2;
// ...
assertion
out := Line1.out or Line2.out;
end
class MotorPump
// description of the motor pump.
end
block System
// ...
MotorPump P1; // 1st instance
MotorPump P2; // 2nd instance
// ...
end
- Классы и экземпляры
- Часто некоторые компоненты моделирования повторно используются от модели к модели. После этого можно создавать библиотеки готовых компонентов моделирования и воплощать их в модели. Для этого используются классы. Это просто контейнеры (или прототипы), определенные вне модели. Экземпляры классов, также называемые объектами, являются клонами этих контейнеров, определенных вне модели.
- Наследование
- Это механизм, с помощью которого специализируются компоненты моделирования. Если производный компонент наследует от базового компонента B , все элементы моделирования B воспроизводятся в D. D D может объявлять дополнительные порты, соединения и контейнеры.
- Агрегация
- Клонирование и создание экземпляров создают компоненты внутри компонентов. Внутренний компонент является частью внешнего. Однако бывают случаи, когда компонент используется другим, не являясь частью этого компонента. Этот механизм отражается в модели с помощью механизма, называемого агрегацией. Агрегация чрезвычайно полезна для проецирования функциональной архитектуры на физическую и для представления так называемых функциональных цепочек. [37]
AltaRica 3.0 включает в себя несколько других конструкций, таких как мощный механизм синхронизации событий. Однако самое важное было представлено выше.
Добавление S2ML поверх математической структуры (GTS в случае AltaRica) позволяет автоматически и бесплатно перейти от разработанной модели, отражающей архитектуру изучаемой системы, к модели, оцененной на основе которой расчеты показателей и моделирование могут выполняться эффективно.
Преобразование сохраняет семантику моделей и по большей части обратимо: результаты расчетов и моделирования можно непосредственно интерпретировать в модели так, как она задумана.
Недавней тенденцией в сообществе AltaRica является разработка шаблонов моделирования. [38] Паттерны широко распространены в инженерии. Они были разработаны, например, в области архитектуры технических систем, [39] а также в области разработки программного обеспечения. [40] Они также полезны при проектировании надежности, поскольку упрощают проектирование и обслуживание моделей. Они также являются инструментом, позволяющим аналитикам рисков сообщать о моделях, которые они разрабатывают и которыми делятся.
Инструменты и приложения [ править ]
В производственной практике модель AltaRica использует четыре основные функции:
- Выработать общее понимание среди заинтересованных сторон о том, как система работает и может потерпеть неудачу.
- Убедитесь, что исследуемая система достаточно безопасна для работы.
- Оптимизация политики обслуживания
- Оцените средний объем производства (или производственных потерь) единиц, подверженных сбоям, неисправностям или человеческим ошибкам.
Поскольку эти приложения требуют различных типов моделирования и расчетов, было разработано несколько инструментов, в том числе:
- Пошаговые симуляторы, интерактивно воспроизводящие сценарии эволюции.
- Компиляторы, использующие формализмы моделирования более низкого уровня, в первую очередь деревья отказов, а также цепи Маркова, в целях использования существующих эффективных алгоритмов оценки.
- Стохастические симуляторы, рассчитывающие широкий спектр индикаторов риска
- Генераторы последовательностей и средства проверки моделей, которые проверяют модели и извлекают сценарии критических сбоев.
Ссылки [ править ]
- ^ Синьоре, Жан-Пьер (июнь 1998 г.). «Язык Алтарики». ESREL, Материалы конференции Европейской ассоциации безопасности и надежности .
- ^ Пойнт, Джеральд (1999). «АльтаРика: автоматы с ограничениями как язык описания». Европейский журнал автоматизированных систем .
- ^ Арнольд, Андре (2000). «Формализм алтарики для описания параллельных систем». Фундамента информатики .
- ^ Пойнт, Джеральд (2000). АльтаРика: Вклад в унификацию формальных методов и эксплуатационной безопасности (Диссертация). Университет LaBRI Бордо I.
- ^ Пойнт, Джеральд (2000). АльтаРика: Вклад в унификацию формальных методов и эксплуатационной безопасности (Диссертация). Университет LaBRI Бордо I.
- ^ Арнольд, Андре (2000). «Формализм алтарики для описания параллельных систем». Фундамента информатики .
- ^ Пойнт, Джеральд (1999). «АльтаРика: автоматы с ограничениями как язык описания». Европейский журнал автоматизированных систем .
- ^ Арнольд, Андре (1994). Конечные переходные системы . Река Аппер-Сэдл, Нью-Джерси: CAR Hoare. Прентис Холл.
- ^ ван Хентенрик, Паскаль (1989). Удовлетворение ограничений в логическом программировании . Кембридж, Массачусетс, США: MIT Press.
- ^ Кунц, Фабьен (2011). «Модельная диагностика систем авионики с использованием минимальных разрезов». Материалы 22-го семинара по принципам диагностики (DX-2011) : 138–145.
- ^ Гриффо, Ален (2004). «Модель-проверщик mec 5». Материалы 16-й Международной конференции по компьютерной верификации (CAV 2004), том 3114 конспектов лекций по информатике : 488–491.
- ^ Гриффо, Ален (2004). «Формальная проверка моделей AltaRica». Гермес, редактор, Труды Конгресса по управлению рисками и эксплуатационной безопасности, Lambda-Mu'14 .
- ^ Винсент, Эмерик (2003). Проектирование и создание средства проверки моделей AltaRica (Диссертация). Университет Бордо.
- ^ Буато, Мари (2006). «Используемый язык потока данных AltaRica: оценка производственной доступности системы с несколькими состояниями». Инженерия надежности и системная безопасность . дои : 10.1016/j.ress.2004.12.004 .
- ^ Рози, Антуан (2002). «Режимы автоматов и их компиляция в деревья отказов». Инженерия надежности и системная безопасность . 78 : 1–12. дои : 10.1016/S0951-8320(02)00042-X .
- ^ Бернар, Ромен (2008). «Уточнение Altarica для анализа модели неоднородной детализации». Акты конгрессов Lambda-Mu'16 .
- ^ Куайзин, Ксавье (2009). «Моделирование производительности миссии наблюдения». Материалы ежегодного симпозиума по надежности и ремонтопригодности .
- ^ Бибер, Пьер (2008). «Интеграция формального анализа ошибок в утверждение: тематические исследования и извлеченные уроки». Материалы 4-го Европейского конгресса по встроенному программному обеспечению реального времени, ERTS 2008 .
- ^ Бернар, Ромен (2007). «Эксперименты по модельному анализу безопасности: управление полетом». В Жан-Марке Форе (ред.). Материалы семинара МФБ по надежному управлению дискретными системами . стр. 43–48.
- ^ Комбе, Тимоти (2011). Моделирование распространения неисправностей в производственных системах (Диссертация). Национальный институт прикладных наук Лиона и Национальная высшая политехническая школа Яунде.
- ^ Аделина, Ромен (2011). Методы проверки формальных моделей эксплуатационной безопасности и их распространения на мультифизические задачи (Диссертация). Университет Тулузы.
- ^ Бернар, Ромен (2009). Мультисистемный анализ безопасности (Диссертация). Университет Бордо.
- ^ Сагаспе, Лоран (2008). Безопасное распределение в авиационных системах: моделирование, проверка и генерация (Диссертация). Университет Бордо.
- ^ Гумберт, Софи (2008). Разбивка требований безопасности от уровня системы до уровня программного обеспечения с помощью формальных моделей (Диссертация). Университет Бордо И.
- ^ Танг Хуу, Минь (2008). Вклад в ускорение стохастического моделирования на моделях потока данных AltaRica (Диссертация). Университет Средиземноморья (Экс-Марсель II).
- ^ Керен, Кристоф (2005). Формальные основания системной архитектуры эксплуатационной безопасности (Диссертация). Национальная высшая школа аэронавтики и космоса (СУПАЭРО).
- ^ Паджетти, Клэр (2004). Расширение языка AltaRica в реальном времени (Диссертация). Центральная школа Нанта и Нантский университет.
- ^ Сен-Жорж, Бенедикт; Мейлланд, Дэвид (2023). «Оценка надежности спутниковой группировки по окончании срока службы с помощью AltaRica 3.0». Инженерные технологии . doi : 10.51257/a-v1-re451 .
- ^ Батте, Мишель (2019). «Алтарика 3.0 в 10 схемах моделирования» . Международный журнал критических компьютерных систем . дои : 10.1504/IJCCBS.2019.098809 .
- ^ Батте, Мишель (2017). «АльтаРика 3.0: спецификация языка». Ассоциация АльтаРика.
{{cite web}}
: Отсутствует или пусто|url=
( помощь ) - ^ Рози, Антуан (2008). «Системы охраняемых переходов: новый формализм состояний/событий для исследований надежности». Журнал риска и надежности .
- ^ Батте, Мишель (2017). «Утверждения Altarica 3.0: почему и зачем». Журнал риска и надежности .
- ^ Рози, Антуан (2019). «Основы модельного системного проектирования и модельной оценки безопасности». Системная инженерия . 22 (2): 146–155. дои : 10.1002/sys.21469 . S2CID 145040668 .
- ^ Батте, Мишель (2018). «От моделей структур к структурам моделей». Международный симпозиум по системной инженерии IEEE (ISSE) 2018 (PDF) . стр. 1–7. дои : 10.1109/SysEng.2018.8544424 . ISBN 978-1-5386-4446-1 . S2CID 54222705 .
- ^ Благородный, Джеймс (1990). Программирование на основе прототипов: концепции, языки и приложения . Спрингер-Верлаг.
- ^ Абади, Маурисио (1998). Теория объектов . Спрингер-Верлаг.
- ^ Вуарен, Жан-Люк (2008). «9.1.1 Метод и инструменты для проектирования систем с ограничениями». Международный симпозиум INCOSE . 18 : 775–789. дои : 10.1002/j.2334-5837.2008.tb00857.x . S2CID 111113361 .
- ^ Батте, Мишель (2019). «Алтарика 3.0 в 10 схемах моделирования» . Международный журнал критических компьютерных систем . дои : 10.1504/IJCCBS.2019.098809 .
- ^ В. Майер, Марк (2009). Искусство системного проектирования . Бока-Ратон: CRC Press.
- ^ Гамма, Эрих (1994). Шаблоны проектирования — элементы многоразового объектно-ориентированного программного обеспечения . Серия профессиональных вычислений Аддисона-Уэсли. Аддисон-Уэсли.