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

В статье описывается архитектура модульной системы трассировки (журнализации, логгирования) и анализа трасс, поддерживающей трассировку сложноструктурированной информации, расширение видов трассируемой информации, изоляцию и выборку нужных данных при анализе полученных трасс и облегчающей связывание разнородных данных между собой. Рассматриваются методы связывания данных, в том числе разнородных, по содержанию и по времени, а также дальнейшего преобразования их в разнообразные отчёты. Описывается архитектура генератора отчётов, позволяющая собирать отчёты из независимых модулей и связывать извлечённые ими данные.

Статья относится к области системного функционального (core-level) тестирования микропроцессоров, более точно модулей управления памяти. В статье описывается метод построения тестов (тестовой программы) для нацеленной генерации. Такая генерация предполагает систематичное построение тестов специального вида. В конце приводятся результаты апробации реализации метода для тестирования модулей управления памяти микропроцессоров архитектуры MIPS64.

В данной статье рассматривается предложенный авторами подход к разработке модулей поддержки архитектур для среды TrEx на основе языка описания процессорных архитектур. Проанализированы достоинства и недостатки подхода по сравнению с уже существующими методами разработки.

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

В данной статье поднята проблема системного тестирования взаимосвязанных модулей аппаратуры, когда их сложность уже не позволяет применять подходы к тестированию на уровне модулей. В работе приводится краткий анализ возможностей построения тестовой системы на основе использования формальных спецификаций, а также предлагается метод верификации, являющийся расширением модульного подхода, основанного на технологии UniTESK.

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

Статья посвящена разработке тестового набора для проверки соответствий реализаций узлов Интернет спецификациям нового протокола безопасности IPsec v2 [1-7]. Для построения тестового набора использовалась технология автоматического тестирования UniTESK [8] и программный пакет CTesK [9], реализующий эту технологию. Работа выполнялась в Институте системного программирования РАН в рамках проекта «Верификация функций безопасности протокола нового поколения IPsec v2» при поддержке гранта РФФИ № 07-07-00243. В ходе ее выполнения были выделены требования к реализациям IPsec v2, разработаны формальные спецификации и прототип тестового набора для верификации реализаций IPsec v2, в том числе реализаций протокола автоматического создания контекстов безопасности IKEv2. В статье описаны метод формализации требований IPsec v2, процесс создания тестового набора, а также результаты тестирования существующих реализаций. Эти результаты показывают, что предложенный в данной работе метод верификации позволяет эффективно автоматизировать тестирование таких сложных протоколов, как протоколы безопасности.

Статья посвящена тестированию соответствия (конформности) реализации требованиям спецификации. Идея безопасного тестирования, предложенная авторами для конформности, основанной на трассах наблюдений, распространяется на случай (слабой) симуляции - конформности, основанной на соответствии состояний реализации и спецификации. Строится теория безопасной симуляции и ее тестирования. Предлагаются общий алгоритм полного тестирования и его модификация для практического применения, опирающаяся на некоторые ограничения на реализацию и спецификацию.

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

В статье описывается разработанная в ИСП РАН система моделирования распределенных вычислительных сред Grid. С помощью этой системы проведен анализ реальной вычислительной среды Sharcnet. На основе анализа были выявлены возможные способы существенного увеличения эффективности работы среды.