Journal influence
Bookmark
Next issue
Monitor oriented programming as a part of controlled execution
The article was published in issue no. № 2, 2010Abstract:Formal methods of verification based on static code analysis, theorem proving and model verification do not describe quantitative characteristics of applications. This article presents the novel approach including the static analysis of a program code, model validation and dynamic verification of the program properties during runtime
Аннотация:Формальные методы верификации программ, основанные на статической проверке соответствия модели, дока-зательстве теорем, статическом анализе, не позволяют в полной мере решать задачи, связанные с контролем количе-ственных характеристик выполнения приложений. В статье предлагается подход, включающий как статический анализ программного кода на соответствие модели, так и динамическую верификацию программы в ходе ее выполнения.
Authors: Galatenko V.A. (galat@niisi.msk.ru) - Scientific Research Institute for System Studies of the Russian Academy of Sciences (SRISA RAS), Moscow, Russia, Ph.D, Kostyukhin K.A. (kost@niisi.msk.ru) - Scientific Research Institute for System Studies of the Russian Academy of Sciences (SRISA RAS), Moscow, Russia, Ph.D, (shmyrev@niisi.msk.ru) - , Ph.D | |
Keywords: distributed systems, the automated information system, controlled execution |
|
Page views: 11620 |
Print version Full issue in PDF (4.97Mb) Download the cover in PDF (1.38Мб) |
Под контролируемым выполнением [1] понимается такая организация функционирования аппаратно-программного комплекса, при которой осуществляются сбор и анализ информации о процессе функционирования и выполняются управляющие воздействия на этот комплекс. Контролируемое выполнение направлено на реализацию комплексом его миссии, несмотря на наличие ошибок и вредоносных воздействий. Понятие контролируемого выполнения включает следующие основные положения: - интеграция средств информационной безопасности, отладки, управления; - наличие целостного набора средств контролируемого выполнения, возможность взаимодействия между ними; - охват всех этапов жизненного цикла аппаратно-программных комплексов, включая этап эксплуатации. В [1] представлена среда контролируемого выполнения (система отладки/мониторинга – СОМ), которая поддерживает возможности интерактивной отладки, мониторинга систем, самоконтроля систем, детерминированного воспроизведения в рамках многопроцессорной конфигурации, применения средств управления информационными системами. Эти возможности позволяют пользователям и разработчикам аппаратно-программных комплексов получать разнообразную информацию о работе приложений и при необходимости выполнять отладочные и управляющие действия. Однако поведение такого рода комплексов описывается множеством сложных взаимозависимых характеристик, поэтому оценка качества функционирования комплекса в целом может быть непростой задачей даже при наличии детальной информации о различных аспектах его выполнения. В данной работе показано развитие концепции контролируемого выполнения, основанное на использовании парадигмы программирования, ориентированного на мониторинг (monitor-oriented programming, MOP [2]). Контролируемое выполнение, основанное на моделировании и верификации Формальные методы верификации программ, основанные на статической проверке соответствия модели, доказательстве теорем, статическом анализе, в силу определенных ограничений [2] не позволяют в полной мере решить задачи, связанные с контролем количественных характеристик выполнения приложений. Авторы предлагают подход, включающий как статический анализ программного кода на соответствие модели, так и динамическую верификацию программы в ходе ее выполнения. В качестве средства описания модели выбран язык C ACSL (ANSI/ISO C SPECIFICATION LANGUAGE [3]), который позволяет описывать поведение программ на языке C в виде аннотаций. Инструмент Why [4] вместе со средствами для доказательства утверждений используется для проверки свойств в статическом режиме. Свойства, задающие количественные характеристики выполнения приложения, описываются с использованием средств профилирования инструментального комплекса СОМ и проверяются динамически в ходе выполнения программы. Механизм динамической верификации основан на парадигме MOP. В данной работе механизмы наблюдения и верификации MOP рассматриваются как компоненты среды контролируемого выполнения. Механизм наблюдения включает средства мониторинга и реализованные в рамках данной работы средства профилирования, позволяющие отслеживать использование приложением целевых ресурсов. Механизм верификации реализован как сопоставление результатов наблюдения с моделью на основе средств самоконтроля. Сбор и анализ информации средствами контролируемого выполнения Контролируемое выполнение подразумевает наличие средств, осуществляющих постоянный сбор информации о ходе работы целевой системы. К их числу относятся средства самоконтроля программ, мониторинга и измерения количественных характеристик (профилирование). Для верификации свойств целевой системы могут использоваться данные, собранные при помощи любых из указанных средств. Библиотека средств самоконтроля (БСС). Реализована в виде набора функций и макровызовов, которые вставляются в исходный текст программы. Разработчик, исходя из логики поведения программы, может встроить в ее код вызовы БСС для выявления признаков некорректного поведения программы. Для таких ситуаций он может предусмотреть вызов отладочных средств, выдачу диагностики или, возможно, корректирующие действия для исправления выявленных отклонений от эталонного правильного поведения. Средства самоконтроля обеспечивают минимальное вмешательство в работу целевой системы, поэтому они широко применяются в приложениях, где важно время выполнения отдельных участков, например обработчиков прерываний, остановка в которых может сделать дальнейшее функционирование бессмысленным. В отличие от средств мониторинга средства самоконтроля не требуют внешних программ для взаимодействия с пользователем. В настоящее время реализован контроль следующих аспектов поведения программ: - изменение хода выполнения программы в результате некорректных значений внутренних переменных программы и входных параметров вызываемых функций; - невозможность завершить выполнение фрагмента кода в установленное время (особенно актуально для контроля приложений в системах реального времени); - сбой в работе программы/системы в результате некорректной работы с динамически выделяемой памятью. Вызовы БСС разделяются на три основные категории: сенсоры, актуаторы и средства протоколирования. Сенсором называется пассивный датчик, фиксирующий изменения в системе на внутреннем уровне. Под актуатором будем понимать активный датчик, имеющий средства реагирования на происходящие изменения. Средства протоколирования доводят до конечного пользователя информацию о состоянии системы и происходящих в ней изменениях. Рассмотрим основные группы вызовов БСС. Актуаторы. Запуск актуаторов осуществляется при помощи вызова UEL_ACTUATOR. Использование актуаторов позволяет проверить значение некоторого выражения и в зависимости от результата выполнить определенные отладочные действия. Если значение выражения ложно, вызывается стандартный обработчик или обработчик, заданный пользователем. Стандартный обработчик выполняет следующие действия: - помещает в протокол сообщение вида ASSERT (выражение): [имя исходного файла:номер строки]; - генерирует событие типа INVALID_STATE, которое может быть отображено средствами мониторинга инструментального комплекса; - останавливает выполнение потока/процесса, что позволяет осуществить над ним действия интерактивной отладки. Поскольку исключительной ситуации при этом не возникает, возможно продолжение выполнения потока в пошаговом или обычном режиме. Сенсоры. Данная группа делится на следующие типы. · Будильник. Сенсоры этого типа позволяют проверить, укладывается ли некоторая последовательность вычислений в заданный временной интервал. Сенсор UEL_SENSOR_GUARD (START) устанавливает интервал времени в секундах. Если за это время управление не достигает вызова UEL_SENSOR_GUARD (STOP), в протокол помещается соответствующее сообщение и генерируется событие, отображаемое средствами мониторинга. · Профилирование. Сенсоры этого типа отмечают начало (UEL_SENSOR_PROFILER (START)) и конец (UEL_SENSOR_PROFILER (STOP)) профилируемого участка кода. Время выполнения участка (вместе с текстовым описателем) выводится в протокол. · Контроль использования динамически распределяемой памяти. Функции запроса и освобождения памяти UEL_calloc, UEL_malloc, UEL_realloc и UEL_free аналогичны стандартным, но регистрируют проходящие через них объекты, сохраняя их адреса, размеры и позицию исходного кода, где они были вызваны. Они также порождают событие INVALID_STATE и выдают в протокол сообщения в случае некорректных ситуаций, например, если функции UEL_free или UEL_realloc передан указатель на свободную память. Сенсор UEL_SENSOR_CHECK_MEMORY_INTEGRITY позволяет запомнить текущее состояние памяти, а позже вывести в протокол отчет об изменениях с момента последнего сохранения. · Динамическая проверка указателей. Сенсоры типа UEL_SENSOR_CHECK_MEMORY_ACCESS служат для проверки корректности указателей. Их можно использовать, например, для проверки аргументов функции в сочетании с актуатором. Возвращаемые значения – UEL_ERR (ошибка при проверке), UEL_BAD (некорректный указатель), UEL_GOOD (корректный указатель). При помощи вызовов данной группы можно проверить, что указатель содержит адрес корректной для потока области памяти, содержащей программный код, из которой можно прочесть заданное число байтов, в которую можно записать заданное число байтов или в которой находится строка печатных символов заданной длины (или до символа конца строки). Средства протоколирования. В любой точке программы можно вывести отчет о текущем состоянии динамически распределяемой памяти с помощью вызова UEL_LOG_MEMORY. Чтобы поместить интересующую пользователя информацию в протокол, надо воспользоваться вызовом UEL_LOG_EXPRESSION. Вызов UEL_LOG_DEBUG_ONLY служит для вычисления заданного выражения только при включенной отладке. Таким способом удобно задавать, например, отладочную печать. Прочее. UEL_init, UEL_fini – инициализация и терминирование БСС. Такой набор функций БСС был выбран авторами на основе опыта, полученного при отладке распределенных приложений. Некоторые компоненты приложений работают под управлением системы реального времени. В частности, необходимо иметь средства контроля времени выполнения определенных фрагментов кода, причем как пассивные (сенсоры), так и активные (актуаторы), реагирующие на соответствующие данные сенсоров. Контроль изменения и доступа к памяти необходим, если отлаживается приложение, активно использующее память, то есть практически любое довольно большое приложение. Механизмы, предоставляющие различные вспомогательные средства (например, средства протоколирования), удобно использовать при управлении отладкой (их можно одновременно включить или выключить одним действием). Система профилирования. В рамках инструментального комплекса СОМ создана система профилирования целевых систем, функционирующих в условиях дефицита ресурсов. Возможности данной системы включают в себя: - поддержку единого способа хранения информации, получаемой из разных источников (система профилирования должна интегрироваться в инструментальный комплекс СОМ, работающий с разными источниками информации, такими как агенты мониторинга, профилирования и т.п.); - сбор количественных характеристик, а именно: · процессорное время для выполнения определенных фрагментов кода программы, · память, используемая программой, · аппаратные события (при их наличии), возникающие в ходе выполнения программы, · сетевые интерфейсы, используемые программой; - использование аппаратных возможностей профилирования при условии наличия соответствующей поддержки; - использование стандартных средств и механизмов для возможности последующей интеграции с существующими решениями. В силу специфики рассматриваемого класса целевых систем понятие профилирования в данной работе используется в более широком смысле, чем сбор информации только об использовании процессорного времени. Под профилированием понимается сбор любых количественных характеристик выполнения приложения, связанных с расходованием ресурсов вычислительной среды, таких как память, полоса пропускания сети и др. Результаты профилирования служат входными данными для средств верификации, осуществляющих сравнение фактического поведения приложения с эталонным. Помимо этого, они могут использоваться традиционным способом, то есть для построения профилей с целью оптимизации приложений, что особенно важно, если целевой аппаратно-программный комплекс содержит узлы, работающие в реальном масштабе времени в условиях дефицита ресурсов. С этой точки зрения важно, чтобы результат работы средств профилирования был представлен в унифицированном формате, позволяющем использовать не только средства инструментального комплекса, осуществляющего контролируемое выполнение целевой системы, но и внешние инструменты обработки данных профилирования. Необходимо также использовать стандартизованные (в том числе аппаратные) интерфейсы для получения информации о ходе выполнения программы, а именно: интерфейсы доступа к аппаратным счетчикам событий процессора, стандартные библиотеки компилятора и целевой ОС, обеспечивающие поддержку построения профилей выполнения программы. Применение стандартизованных подходов, существующих в различных предметных областях, является одной из важных характеристик среды контролируемого выполнения, поскольку это повышает переносимость ее инструментальных средств и позволяет наращивать функциональность за счет применения средств сторонних разработчиков. На основании изложенного можно сделать следующие выводы. В представленной работе понятие контролируемого выполнения расширено за счет внедрения парадигмы программирования, ориентированного на мониторинг, введения средств динамического моделирования целевых аппаратно-программных комплексов, а также новых средств профилирования. Под профилированием в контексте данной работы понимаются сбор и анализ информации о различных количественных характеристиках выполнения комплексов, включая данные об использовании как процессорного времени, так и других целевых ресурсов. Необходимость введения этих средств продиктована и сложностью рассматриваемых аппаратно-программных комплексов, и критичностью предъявляемых к ним требованиям по обеспечению должного качества обслуживания. Литература 1. Костюхин К.А. Организация контролируемого выполнения для разнородных распределенных программно-аппаратных комплексов. М.: НИИСИ РАН, 2006. 2. Chen F., Rosu G. MOP: Reliable software development using abstract aspects: Tech. rep.: Dept. of Computer Science, University of Illinois, 2006. 3. Baudin P., Filliatre J.-C., Marche C. Et al. ASCL: ANSI/ISO C Specification Language, 2008. 4. Filliatre J.-C., Marche C. The why/krakatoa/caduceus platform for deductive program verification, OOPSLA, 2004. |
Permanent link: http://swsys.ru/index.php?id=2501&lang=en&page=article |
Print version Full issue in PDF (4.97Mb) Download the cover in PDF (1.38Мб) |
The article was published in issue no. № 2, 2010 |
Perhaps, you might be interested in the following articles of similar topics:
- Математическая модель контролируемого выполнения
- Проблемы отладки многопроцессных систем
- Разработка прецедентного модуля для идентификации сигналов при акустико-эмиссионном мониторинге сложных технических объектов
- Возможности мониторинга динамики развития проекта в интеллектуальном проектном репозитарии
- Математическое моделирование распределенных систем защиты информации
Back to the list of articles