<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Использование методов модельно-ориентированной обратной разработки для анализа ARINC 653 совместимого функционального ПО</article-title>
      </title-group>
      <fpage>247</fpage>
      <lpage>255</lpage>
      <abstract>
        <p>This paper is dedicated to methods of Model-Driven Reverse Engineering for avionics software analysis. An algorithm for building architecture models from source code of application software is described in this paper. Architecture Analysis &amp; Design Language is used as a target language for architecture modeling. We consider ARINC 653-compatible application software for models building. The algorithm implementation is based on CPAchecker static analyzer. Аннотация. Исследуется применение методов модельноориентированной обратной разработки для анализа программного обеспечения (ПО) для авионики. Описывается алгоритм построения архитектурных моделей по исходному коду функционального ПО. Для описания архитектурных моделей используется язык AADL (Architecture Analysis &amp; Design Language). Для построения моделей рассматривается ARINC-653 совместимое ПО. Предложенный алгоритм реализован на базе инструмента статического анализа CPAchecker.</p>
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>-</title>
      <p>
        лирования используется язык AADL (Architecture Analysis &amp; Design Language).
Для построения моделей используется функциональное ПО для авионики,
которое соответствует спецификации ARINC 653[
        <xref ref-type="bibr" rid="ref3">3</xref>
        ].
      </p>
      <p>
        Целью данной работы является разработка и реализация алгоритма
построения архитектурных моделей в формате AADL на основе автоматического
анализа исходного кода функционального ПО на языке С для ARINC 653
совместимых ОС. В работе рассматривается двухэтапный алгоритм построения
архитектурной модели функционального ПО. На первом этапе производится анализ
исходного кода ПО и определяются ARINC 653 сущности и их связи. На втором
этапе ARINC 653 сущности трансформируются в AADL модель. Предложенный
алгоритм реализован на базе инструмента статического анализа CPAchecker [
        <xref ref-type="bibr" rid="ref4">4</xref>
        ].
2
      </p>
      <p>Анализ исходного кода
Исследуемое функциональное ПО предоставляется в виде файлов с исходными
кодами на языке С, в которых используются вызовы функций ОС,
определенные спецификацией ARINC 653. Для демонстрации особенностей работы
алгоритма используется пример программы, в которой создаются три процесса и
четыре порта. Каждый из процессов реализует свою логику работы с портами. В
листинге 1 представлен фрагмент ПО, в котором создается один процесс.</p>
      <p>static PROCESS_ID_TYPE pid_P1, pid_P2, pid_P3;
...</p>
      <p>PROCESS_ATTRIBUTE_TYPE P1_process_attrs = {
.PERIOD = 63000000LL,
.TIME_CAPACITY = 63000000LL,
.STACK_SIZE = 8096,
.BASE_PRIORITY = 1,
.DEADLINE = SOFT,
};
P1_process_attrs.ENTRY_POINT = shared_process2;
strncpy(P1_process_attrs.NAME, "P1_process",
sizeof(PROCESS_NAME_TYPE));
CREATE_PROCESS(&amp;P1_process_attrs,&amp;pid_P1,&amp;ret_process);
Листинг 1. Создание ARINC 653 процесса.</p>
      <p>Создание процесса происходит с помощью вызова функции
CREATE_PROCESS, которой в качестве первого аргумента передается
структура, содержащая атрибуты создаваемого процесса. В листинге 1 для задания
атрибутов процесса используется переменная P1_process_attrs с типом
PROCESS_ATTRIBUTE_TYPE. Поле ENTRY_POINT содержит указатель на
потоковую функцию, т.е. функцию, которой передается управление при старте
процесса. В рассматриваемом примере программы явный вызов потоковой
функции shared_process2 отсутствует, при этом поле ENTRY_POINT содержит
указатель на потоковую функцию, что позволяет ОС неявно вызывать
потоковую функцию при выполнении программы. Для проведения анализа потоковой
функции в рамках рассматриваемого алгоритма вызов потоковой функции
искусственно добавляется уже на этапе анализа программы.</p>
      <p>
        Перед началом анализа программы CPAchecker преобразует исходный код
анализируемой программы в автомат потока управления — Control-Flow
Automaton (CFA). CFA представляет собой направленный граф, узлы которого
соответствуют точкам в программе, а ребра — операциям. Анализа исходного
кода программы выполняется за два прохода. При первом проходе
определяются все создаваемые процессы и их атрибуты. При втором проходе происходит
искусственное добавление вызовов всех используемых потоковых функций
непосредственно в CFA перед последней программной инструкцией функции
main. Для определения фактических значений переменных в любой точке
программы используется алгоритм анализа явных значений (explicit-value analysis)
[
        <xref ref-type="bibr" rid="ref5">5</xref>
        ].
static void first_process(void) {
      </p>
      <p>shared_process(true, false);
}
static void second_process(void) {</p>
      <p>shared_process(true, true);
}
static void third_process(void) {</p>
      <p>shared_process(false, true);
}
static void shared_process(bool read, bool write) {
if (read) {</p>
      <p>READ_FROM_SAMPLING_PORT(RT);
}
if (write) {</p>
      <p>WRITE_TO_SAMPLING_PORT(WAZ);
При анализе потоковой функции, используемой несколькими процессами,
может потребоваться информация о том, какому именно процессу она
принадлежит. При создании процесса операционная система назначает ему
идентификатор. В дальнейшем идентификатор текущего потока можно узнать с помощью
вызова функции ОС GET_MY_ID. Учитывая, что при статическом анализе
реальных вызовов функций ОС не происходит, на этапе анализа в программу
вводится искусственная переменная $PID, в которой хранится идентификатор
текущего процесса.
void CREATE_PROCESS (</p>
      <p>PROCESS_ATTRIBUTE_TYPE
PROCESS_ID_TYPE
RETURN_CODE_TYPE
*attributes,
*process_id,
*return_code)
Листинг 3. Прототип функции создания ARINC 653 процесса.</p>
      <p>Для того чтобы определить какому именно процессу принадлежит потоковая
функция при ее вызове в программе в CFA непосредственно перед ее вызовом
добавляется операция присваивания переменной $PID значения
идентификатора текущего процесса. На рисунке 1 представлен фрагмент CFA в графическом
формате.
Рис. 1. Фрагмент автомата потока управления (CFA) программы.
static void shared_process2(void) {</p>
      <p>RETURN_CODE_TYPE ReturnCode;
PROCESS_ID_TYPE MyId;
GET_MY_ID ( &amp;MyId, &amp;ReturnCode );</p>
      <p>if (MyId == pid_P1) {
READ_FROM_SAMPLING_PORT(RT);</p>
      <p>WRITE_TO_SAMPLING_PORT(WAZ);
Для рассматриваемого примера, в котором используется потоковая функции
shared_process2, с помощью предложенного алгоритма анализа было
определено, что:
1. в программе создаются три ARINC 653 потока и четыре порта;
2. первый поток обращается к порту RT на чтение и к порту WAZ на запись;
3. второй поток обращается к порту RDELTAE на чтение и к порту WQ на
запись;
4. третий поток обращается к портам RT и RDELTAE на чтение и к портам</p>
      <p>WAZ и WQ на запись.</p>
      <p>Информация, полученная в результате анализа исходного кода, сохраняется
в программе во внутреннем формате и используется в дальнейшем при
построении архитектурной модели. В следующем разделе будет описан второй этап
алгоритма — этап построения архитектурной модели.
3</p>
      <p>Построение архитектурной модели
На втором этапе на основании информации об имеющихся ARINC 653 объектах
и логических связей между ними строится AADL модель. ARINC 653 сущности
преобразуются в элементы AADL модели по определенным правилам: ARINC
653 раздел соответствует AADL процессу, ARINC 653 процесс соответствует
AADL потоку, ARINC 653 порты без очереди (SAMPLING PORT)
отображаются в AADL модели с помощью компонента data порт, порты с очередью
(QUEUING PORT) отображаются в AADL модели с помощью компонента event
data порт.</p>
      <p>Рис. 2. Графическое представление AADL модели.
thread P1_process
features</p>
      <p>RT: in data port {Source_Name =&gt; RT;</p>
      <p>ARINC653::Sampling_Refresh_Period =&gt; 100 ms;};
WAZ: out data port {Source_Name =&gt; WAZ;</p>
      <p>ARINC653::Sampling_Refresh_Period =&gt; 100 ms;};
properties
Source_Stack_Size =&gt; 8096 Bytes;
Priority =&gt; 1;
Period =&gt; 63 ms;</p>
      <p>Compute_Deadline =&gt; 63 ms;
end P1_process;</p>
      <p>Листинг 5. AADL поток.</p>
      <p>В листинге 5 представлен фрагмент AADL модели в текстовом формате,
содержащий описание AADL потока, который соответствует ARINC 653 процессу
из листинга 1. В листинге 6 представлен фрагмент AADL модели содержащий
реализацию AADL процесса. AADL процесс состоит из трех AADL потоков,
которые соответствуют трем ARINC 653 процессам, использующим одну и ту
же потоковую функцию shared_process2 из листинга 4. Эта потоковая функция
устанавливает разные правила работы с портами для разных ARINC 653
процессов.
process implementation main_process.impl
subcomponents</p>
      <p>P1_process: thread P1_process.impl;
P2_process: thread P2_process.impl;</p>
      <p>P3_process: thread P3_process.impl;
connections
con0: port RT -&gt; P1_process.RT;
con1: port P1_process.WAZ -&gt; WAZ;
con2: port RDELTAE -&gt; P2_process.RDELTAE;
…</p>
      <p>Листинг 6. Фрагмент AADL процесса.</p>
      <p>Полученная архитектурная модель может использоваться для дальнейшего
анализа и проектирования системы с помощью любого инструмента,
поддерживающего спецификацию AADL версии 2.1. В данной работе был использован
инструмент MASIW [6], который предназначен для проектирования и анализа
систем интегрированной модульной авионики. На рисунке 2 представлено
графическое представление AADL модели полученное с помощью инструмента
MASIW.</p>
      <p>Оценка производительности
Для оценки производительности алгоритма необходимо исследовать время
выполнения этапа анализа исходного кода, на который приходятся основные
временные затраты работы алгоритма. На рисунке 3 представлено три графика,
отражающие зависимость среднего времени анализа исходного кода от сложности
Рис. 3. График зависимости времени анализа исходного кода от сложности ПО.
анализируемого функционального ПО. Сложность ПО определяется
количеством создаваемых ARINC 653 процессов и количеством используемых
ресурсов (портов) в потоковой функции каждого процесса. Для исследования
использовалось функциональное ПО, в котором количество ARINC 653 процессов
последовательно увеличивалось с двух до тридцати двух с шагом два. Кроме
этого, для каждого варианта конфигурации ПО, в котором количество
процессов зафиксировано, использовались три разные потоковые функции: первая
потоковая функция обращается к двум портам (нижний график), вторая – к
четырем (средний график) и третья – к восьми (верхний график). Из графика
видно, что при использовании самой простой конфигурации ПО среднее время
выполнения этапа анализа исходного кода составляет около 100 миллисекунд.
При использовании самой сложной конфигурации ПО среднее время
выполнения этапа анализа исходного кода составляет немного больше одной
секунды (1067 миллисекунд). Для всех остальных промежуточных
конфигураций ПО значение среднего времени анализа не выходило за пределы
диапазона значений от 100 до 1067 миллисекунд. Измерения проводились на
компьютере с операционной системой GNU/Linux (Ubuntu 16.04) x86_64 с</p>
      <p>Заключение
В данной работе представлен двухэтапный алгоритм построения архитектурных
моделей в формате AADL на основе автоматического анализа исходного кода
функционального ПО для ARINC 653 совместимых ОС. Предложенный
алгоритм реализован в виде отдельного модуля для статического анализатора
CPAchecker. Работа алгоритма продемонстрирована на тестовом приложении
для ARINC 653 совместимой операционной системы.
Литература</p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <given-names>SAE</given-names>
            <surname>International standard</surname>
          </string-name>
          <string-name>
            <surname>AS5506C</surname>
          </string-name>
          ,
          <source>Architecture Analysis &amp; Design Language (AADL)</source>
          ,
          <year>2017</year>
          . http://standards.sae.org/as5506c/.
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2. SAE International standard AS5506/1A,
          <string-name>
            <given-names>Architecture</given-names>
            <surname>Analysis</surname>
          </string-name>
          &amp; Design
          <string-name>
            <surname>Language (AADL)</surname>
            ,
            <given-names>A</given-names>
            nnex A
          </string-name>
          : ARINC653 Annex,
          <year>2015</year>
          . http://standards.sae.org/as5506/1a/.
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3. ARINC.
          <source>ARINC Specification 653P1-3: Avionics Application Software Standard Interface Part</source>
          <volume>1</volume>
          -
          <string-name>
            <given-names>Required</given-names>
            <surname>Services. Aeronautical Radio</surname>
          </string-name>
          <string-name>
            <surname>INC</surname>
          </string-name>
          , Maryland, USA,
          <year>2010</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <surname>Beyer</surname>
            <given-names>D.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Keremoglu</surname>
            <given-names>M.E.</given-names>
          </string-name>
          <article-title>CPAchecker: A Tool for Configurable Software Verification</article-title>
          . In Gopalakrishnan, G.,
          <string-name>
            <surname>Qadeer</surname>
            ,
            <given-names>S. (eds.) CAV</given-names>
          </string-name>
          <year>2011</year>
          .
          <article-title>LNCS</article-title>
          , vol.
          <volume>6806</volume>
          , pp.
          <fpage>184</fpage>
          -
          <lpage>190</lpage>
          . Springer, Heidelberg,
          <year>2011</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          5.
          <string-name>
            <surname>Beyer</surname>
            <given-names>D.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Löwe</surname>
            <given-names>S.</given-names>
          </string-name>
          :
          <article-title>Explicit-value analysis based on CEGAR and interpolation</article-title>
          .
          <source>Technical Report MIP-1205</source>
          , University of Passau / ArXiv 1212.6542,
          <year>December 2012</year>
          .
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>