Способ статической оценки времени работы компонентов AADL-моделей

При проектировании современных систем авионики, а также других ответственных систем, неотъемлемой частью разработки является моделирование этих систем. Модели могут использоваться для проверок и валидации системы, в том числе на ранних этапах разработки. Ранняя валидация важна из-за того, что стоимость исправления ошибок растёт экспоненциально от времени внесения этой ошибки. Для моделирования такого рода систем широко используется язык моделирования AADL, позволяющий моделировать как архитектуру разрабатываемых систем, так и некоторые поведенческие характеристики компонентов модели. В статье рассматривается задача автоматизированной проверки модели на консистентность некоторых поведенческих свойств. В частности, рассматривается проблема оценки времени работы компонентов моделей и соответствия этого времени другим свойствам в модели. Эта проблема близка к проблеме худшего времени выполнения (WCET), но имеет свою специфику в данном приложении. Рассмотрен статический подход, работающий со стандартной спецификацией поведения компонентов AADL-моделей специализированными расширенными конечными автоматами. В статье были рассмотрены особенности используемой модели поведения (специализированных конечных автоматов), в частности, за счёт работы автомата со временем и внешними событиями. Были рассмотрены проблемы оценки времени работы таких моделей поведения, связанные с нелокальностью этой характеристики в ряде случаев. Был рассмотрен важный частный случай, а также общий случай этой проблемы. В статье предлагается алгоритм, позволяющий оценить время работы таких моделей поведения в этих случаях. Данные алгоритм реализован и используется в среде разработки AADL-моделей АРМ СИ (MASIW).