Preview

Труды Института системного программирования РАН

Расширенный поиск
Том 26, № 2 (2014)
Скачать выпуск PDF
5-42
Аннотация
Ядро операционной системы (ОС) представляет собой критичную в отношении надежности и производительности программную систему. Качество ядра современных ОС уже находится на достаточно высоком уровне. Иначе обстоит дело с модулями ядра, например, драйверами устройств, которые по ряду причин имеют существенно более низкий уровень качества. Одними из наиболее критичных и распространенных ошибок в модулях ядра являются нарушения правил корректного использования программного интерфейса ядра ОС. Выявить все такие нарушения в модулях или доказать их корректность потенциально можно с помощью инструментов статической верификации, которым для проведения анализа необходимо предоставить контрактные спецификации, описывающие формальным образом обязательства ядра и модулей по отношению друг к другу. В статье рассматриваются существующие методы и системы статической верификации модулей ядра различных ОС. Предлагается новый метод статической верификации модулей ядра ОС Linux, который позволяет конфигурировать процесс проверки на каждом из его этапов. Показывается, каким образом данный метод может быть адаптирован для проверки компонентов ядра других ОС. Описывается архитектура конфигурируемой системы статической верификации модулей ядра ОС Linux, реализующей предложенный метод, и демонстрируются результаты ее практического применения. В заключении рассматриваются направления дальнейшего развития
43-86
Аннотация
Исследование графов автоматами является корневой задачей во многих приложениях. К таким приложениям относятся верификация и тестирование программных и аппаратных систем, а также исследование сетей, в том числе сети интернета и GRID на основе формальных моделей. Модель системы или сети, в конечном счёте, сводится к графу переходов, свойства которого нужно исследовать. За последние годы размер реально используемых систем и сетей и, следовательно, размер их моделей и, следовательно, размер исследуемых графов непрерывно растёт. Проблемы возникают тогда, когда исследование графа одним автоматом (компьютером) либо требует недопустимо большого времени, либо граф не помещается в памяти одного компьютера, либо и то и другое. Поэтому возникает задача параллельного и распределённого исследования графов. Эта задача формализуется как задача исследования графа коллективом автоматов (несколькими параллельно работающими компьютерами с достаточной суммарной памятью). Решению этой задачи посвящена данная работа.
87-96
Аннотация
QEMU - свободное программное обеспечение с открытым исходным кодом, предназначенное для эмуляции различных платформ. В данной статье описывается разработанный способ описания аппаратных конфигураций гостевых систем в эмуляторе QEMU с помощью отдельных текстовых файлов, использующих удобный для чтения и написания текстовый формат JSON. Внешние конфигурационные файлы позволят избежать необходимости перекомпилировать QEMU при любых изменениях аппаратных конфигураций гостевых систем, а также избавят от необходимости разбираться во всех тонкостях внутренней реализации эмулятора.
97-118
Аннотация
В данной работе рассматривается задача анализа помеченных данных. Для её решения предлагается статический межпроцедурный котекстно-потоковый объектно-чувствительный алгоритм, производится оценка характеристик данного алгоритма, обсуждаются особенности реализации на базе компиляторной инфраструктуры LLVM и приводятся результаты практического тестирования
119-136
Аннотация
В данной работе представлен подход к внесению неисправностей в программу, использующий механизм детерминированного воспроизведения в симуляторе. Внесение неисправностей используется для проверки качества покрытия кода тестами, способности системы реагировать на некорректные данные или механизма обработки исключений. При внесении неисправностей предлагается использовать детерминированное воспроизведение работы программ, что позволит упростить инициализацию системы, ускорить ее тестирование с помощью фаззинга, а также изучить альтернативные пути выполнения программы при ее отладке.
137-158
Аннотация
В статье рассматриваются три направления использования информационных технологий в анализе безопасности атомных электростанций (АЭС). Это: динамический вероятностный анализ безопасности АЭС, возможности использования кодов расчетной гидродинамики (CFD) для моделирования сложных процессов ядерных энергетических установок и проблема идентификации аварии на АЭС. Используемые технологии повышают эффективность как обработки информации - генетические алгоритмы (ГА), нейронные сети (НС), так и расчетов - параллельные вычисления. Применение новых технологий основывается на их гармоничном сочетании с существующими классическими методами анализа безопасности АЭС.
159-174
Аннотация
Упрощение полигональных моделей является одной из распространенных методик, позволяющих увеличить скорость растеризации масштабных сцен, состоящих из большого количества сложных объектов. Традиционные алгоритмы, как правило, основанные на последовательном исключении ребер и граней, имеют высокую вычислительную сложность, что является препятствием для реализации ряда графических приложений на CPU. С развитием технологий программирования графического процессора открываются новые возможности для эффективной параллельной реализации данных алгоритмов. В работе обсуждаются некоторые известные алгоритмы упрощения полигональных моделей, использующие возможности распараллеливания независимых операций исключения ребер и спекулятивных оценок визуального качества редуцируемого полигонального представления. Сравниваются основные характеристики описанных алгоритмов и параллельных программ, а также даются рекомендации по их практическому использованию.
175-196
Аннотация
Технологии и системы визуального пространственно-временного моделирования проектов получили распространение в последние годы. Однако невозможность применения к масштабным индустриальным проектам и программам является одним из ключевых факторов, сдерживающим их широкое применение. В работе обсуждаются проблемы эффективности и масштабируемости систем данного класса, а также пути решения на основе индексации проектных данных. Для предложенных схем пространственно-временной индексации и выделенных типов запросов описаны алгоритмы исполнения, а также получены оценки их вычислительной сложности. Полученные оценки подтверждают эффективность и перспективность предложенных схем индексации, а выработанные рекомендации помогают в их практической реализации.
197-230
Аннотация
Статья адресована актуальной проблеме верификации масштабных моделей данных, применяемых в различных индустриальных областях и специфицируемых на популярных универсальных объектно-ориентированных языках, таких как EXPRESS, UML/OCL. Основные преимущества языков информационного моделирования (высокая выразительность, декларативность, богатство синтаксических конструкций) отрицательно сказываются в процессе автоматической верификации спецификаций. Существующие методы верификации моделей вследствие высокой вычислительной сложности не могут использоваться для решения данной проблемы. В статье предлагается комбинированный метод верификации объектно-ориентированных моделей данных, основанный на последовательной редукции к нескольким постановкам математических задач: линейного программирования, удовлетворения ограничений (CSP), выполнимости булевых формул (SAT). Детально исследуется ключевая проблема определения необходимого количества экземпляров для генерации корректной коллекции объектов и ее редукция к задаче целочисленного линейного программирования. Работа поддержана РФФИ (грант 13-07-00390).
231-244
Аннотация
Настоящая работа является продолжением ряда публикаций, посвященных исследованиям методов управления сложными объектами на основе прецедентов. В ситуации, когда трудно или невозможно получить точную математическую модель поведения объекта, целесообразно применять метод управления по прецедентам. Вместо модели мы можем опираться только на доступную информацию о состояниях объекта, управляющих воздействиях на него и результатах воздействий. Такой выбор в теории вывода по прецедентам соответствует трем составляющим понятия “прецедент”: описанию проблемы, примененному решению и исходу - результату применения решения. Подход к управлению основан на разбиении состояний объектов управления на классы, состояния в каждом из которых эквивалентны друг другу с точки зрения управления. Состояние объекта управления сравнивается с прецедентами из заранее накопленной базы данных. Чтобы подобрать воздействие для текущего случая, на основе некоей меры близости в базе прецедентов отыскивается прецедент со схожим исходным и конечным состоянием. Из него заимствуется управляющее воздействие. В основе подходов к построению систем вывода по прецедентам лежит оценка схожести прецедента и текущего случая. В предыдущих публикациях был предложен метод оценки схожести, основанный на разбиении базы прецедентов на классы эквивалентности. Для оценки не полностью описанного случая используются проекции классов на его пространство признаков. Неполнота в описании объекта в условиях дефицита времени и ресурсов приводит к неоднозначности в оценке объекта. Классы, в пересечение которых попадает объект, образуют так называемый дифференциальный ряд объекта. Отсутствие разделяющего классы признака затрудняет выбор управляющего воздействия. Предлагаемая методика позволяет снизить эту неоднозначность, если принять во внимание предысторию объекта - его состояния и реакции на воздействия. Как следствие, ограничивается выбор управляющих воздействий. Описывается способ снижения неоднозначности оценки. Вводится понятие “прогнозируемый” дифференциальный ряд объекта. Итоговая оценка состояния выводится на основе сравнений текущего и прогнозируемого рядов.
245-268
Аннотация
Задача унификации пары подстановок θ_1 и θ_2 состоит в вычислении такой пары подстановок η' и η'', чтобы композиции θ_1 η' и θ_2 η'' были равны. По существу, задача унификации подстановок равносильна задаче решения линейных уравнений вида θ_1 X=θ_2 Y в полугруппе подстановок. Но некоторые линейные уравнения над подстановками также можно рассматривать как новые варианты задачи унификации. В этой статье мы вводим понятие двусторонней унификации как процесса преобразования одной заданной подстановки θ_1 к другой заданной подстановке θ_2 при помощи композиции, применяемой как справа, так и слева к подстановке θ_1. Иначе говоря, задача двусторонней унификации состоит в решении уравнений вида Xθ_1 Y=θ_2. Двусторонняя унификация подстановок может быть использована при решении одной из задач реорганизации (рефакторинга) программ - выделения в заданном фрагменте кода тела библиотечной процедуры с целью последующей замены выделенного участка кода на вызов этой процедуры. В статье исследован вопрос о сложности задачи двусторонней унификации подстановок. Установлено, что эта задача является NP-полной. Доказательство NP-трудности задачи двусторонней унификации проводится путем сведения к ней NP-полной задачи правильного расположения домино в прямоугольной области плоскости. В статье также сформулирована и исследована задача двусторонней унификации программ в модели программ первого порядка с отношением логико-термальной эквивалентности. Доказано, что сформулированная задача двусторонней унификации программ также является NP-полной.
269-274
Аннотация
Защита информации в облачных вычислениях активно исследуется мировым научным сообществом. Эти исследования показали, что обозначенная проблема намного сложнее тех задач защиты информации, которые решаются известными криптографическими средствами. Так, например в работе [1] рассмотрена математическая модель организации облачных вычислений и доказано, что уже в случае двух пользователей защита информации невозможна. Предлагается альтернативная модель организации облачных вычислений, в которой указанный отрицательный результат не имеет места. Исследуются методы защиты информации в этой новой модели.
275-296
Аннотация
В работе М. А. Тайцлина и А. П. Столбоушкина было введено понятие недетерминированной программы, и определен класс языков, распознаваемых недетерминированными программами. Доказана теорема, свидетельствующая о близости этого класса, и NL. Мы исследуем класс языков, определяемый в некоторой модификации указанной вычислительной модели, и доказываем, что рассматриваемый класс языков равен NL.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)