Том 18, № 4 (2011)
Оригинальные статьи
7-20 568
Аннотация
Язык Atoment - предметно-ориентированный язык выполнимых спецификаций, применяемый для описания методов и техник верификации программ. В этой работе представлена коллекция типовых примеров использования языка Atoment, охватывающая такие темы, как модели программ, операционная, трансформационная и аксиоматическая семантики, формальная спецификация языков программирования.
21-33 570
Аннотация
Предложен новый вид аннотаций, называемых атрибутными аннотациями, и методология их применения в дедуктивной верификации программ. Описана коллекция аннотирующих атрибутов для подмножества C-kernel языка C и на их основе представлены два варианта аксиоматической семантики языка C- kernel - семантика прямого прослеживания и смешанная семантика прямого прослеживания.
33-44 486
Аннотация
Односчетчиковые сети представляют собой конечные автоматы с дополнительным целочисленным неотрицательным счетчиком. Переход управляющего автомата увеличивает или уменьшает значение счетчика, при этом уменьшение возможно только в том случае, когда результат будет неотрицательным; проверка на ноль отсутствует. Односчетчиковые сети эквивалентны по выразительной мощности сетям Петри с не более чем одной неограниченной позицией, а также магазинным автоматам с односимвольным стековым алфавитом.
В работе представлен метод приближения наибольшей бисимуляции в односчетчиковой сети, основанный на использовании однопериодической символьной арифметики и понятия расслоенной бисимуляции.
В работе представлен метод приближения наибольшей бисимуляции в односчетчиковой сети, основанный на использовании однопериодической символьной арифметики и понятия расслоенной бисимуляции.
45-55 586
Аннотация
Описано разрабатываемое средство статического анализа программного обеспечения. Основной идеей данного средства является использование систем типов и эффектов для статического анализа реальных программ. Средство использует формат промежуточного представления LLVM в качестве входного представления программы, таким образом, давая возможность анализировать программы на любых языках, поддерживаемых системой LLVM. Разбор указанного формата осуществляется встроенным парсером, позволяющим осуществить формирование внутренней модели программы, схожей с моделью LLVM. Целью создания описываемого средства является исследование возможностей построения методов статического анализа программ на основе известных алгоритмов, использующих системы типов и эффектов, путём применения этих алгоритмов к модели и опосредованно к исходному коду.
56-67 429
Аннотация
Символьная проверка на модели основана на компактном представлении множеств. На данный момент есть три основных направления символьной проверки моделей: методы, основанные на бинарных разрешающих диаграммах, ограниченная проверка моделей, использующая SAT-решатели, и различные алгебраические подходы к эффективному представлению данных. В данной работе предлагается рассмотреть улучшенные алгоритмы манипуляции с алгебраическим представлением данных, а именно алгоритмы оптимизации аффинных представлений данных.
68-79 536
Аннотация
Статья посвящена разработке методов анализа зависимостей с целью повышения точности статического анализа. Рассмотрены причины, ведущие к снижению точности абстрактной интерпретации при обнаружении дефектов в программном коде. На различных примерах показана необходимость выявления и интерпретации зависимостей между программными объектами в ходе анализа. Приведена классификация зависимостей по различным признакам. Показана необходимость совокупного рассмотрения хранимых значений и зависимостей. Описан порядок выявления зависимостей при интерпретации присваиваний. Предложен метод интерпретации зависимостей на основе логического вывода, базирующегося на известных правилах логики и арифметики. Некоторые из разработанных методов реализованы в средстве обнаружения дефектов Digitek Aegis, показано значительное увеличение точности анализа.
80-93 546
Аннотация
Построена ингибиторная сеть Петри с фиксированной структурой, которая выполняет произвольный заданный нормальный алгорифм Маркова. Алгорифм и его входная цепочка шифруются целыми неотрицательными числами и помещаются в выделенные позиции сети Петри, реализующей применение подстановок алгорифма к цепочке символов. Использованы правила кодирования последовательных, ветвящихся и циклических процессов сетями Петри. По завершении работы сети выходная цепочка восстанавливается (дешифруется) из целочисленной формы представления. В парадигме вычислений на сетях Петри построенная сеть обеспечивает совместимость систем.
94-105 500
Аннотация
Модели систем на языке SystemC, как правило, являются параллельными программами и поэтому могут содержать ошибки синхронизации. Одним из типов ошибок синхронизации являются ошибки конкурентной модификации данных.
В данной статье предлагается подход к обнаружению ошибок конкурентной модификации данных в моделях на языке SystemC на основе статического анализа. Разработаны алгоритмы, обеспечивающие анализ программ на языке SystemC без количественного времени. Эти алгоритмы позволяют обнаружить все ошибки конкурентной модификации данных, имеющиеся в программе. Эффективность предложенного подхода подтверждается экспериментальными исследованиями разработанного средства обнаружения ошибок на наборе тестовых программ.
В данной статье предлагается подход к обнаружению ошибок конкурентной модификации данных в моделях на языке SystemC на основе статического анализа. Разработаны алгоритмы, обеспечивающие анализ программ на языке SystemC без количественного времени. Эти алгоритмы позволяют обнаружить все ошибки конкурентной модификации данных, имеющиеся в программе. Эффективность предложенного подхода подтверждается экспериментальными исследованиями разработанного средства обнаружения ошибок на наборе тестовых программ.
106-117 526
Аннотация
Предложен алгоритм решения задачи покрытия для монотонных счетчиковых систем. Разрешимость этой задачи хорошо известна, но данный алгоритм интересен своей простотой. Он возник из упрощения некоторой итеративной процедуры применения суперкомпилятора (специализатора программ, основанного на методе суперкомпиляции В.Ф. Турчина) к программе, кодирующей счетчиковую систему и начальное и целевое множества состояний, и из доказательства, что при определенных условиях эта процедура завершается и решает задачу покрытия.
118-130 551
Аннотация
Рассматривается модель, используемая при ручной разработке спецификаций приложения, созданная на основе теории базовых протоколов А.А. Летичевского и поддерживающего теорию инструментария символьной верификации. Обсуждаются способы ограничения поведенческих характеристик модели при условии сохранения соответствия исходным требованиям. По успешно верифицированной модели генерируется код приложения и код тестов. Приводится описание методики применения разработанной модели.
Наталья Геннадьевна Кушик,
Амель Маммар,
Ана Кавалли,
Нина Владимировна Евтушенко,
Вилли Джиминез,
Эдгардо Монте Де Ока
131-143 720
Аннотация
Предлагается метод тестирования безопасности С программ с использованием широко известного верификатора SPIN. Обсуждаются классы уязвимостей в С программах, которые могут быть обнаружены с использованием предложенного подхода. Приводятся результаты компьютерных экспериментов по обнаружению уязвимостей в студенческих программных реализациях алгоритмов работы с массивами.
144-156 547
Аннотация
Рассматриваются униформные системы взаимодействующих расширенных конечных автоматов, которые удобны для задания исходной спецификации телекоммуникационных систем, таких как кольцевые протоколы и телефонные сети. Цель работы - представить программный комплекс Automata Systems Verifier (ASV), предназначенный для анализа и верификации автоматных спецификаций. Он базируется на алгоритме трансляции систем автоматов в раскрашенные сети Петри (РСП), представленном и обоснованном в [4]. Для анализа РСП комплекс ASV использует систему CPN Tools [10], а для их верификации методом проверки моделей относительно свойств, заданных формулами мю-исчисления, он использует систему Petri Net Verifier [12]. Описано применение этого комплекса к верификации кольцевого RE-протокола и к исследованию взаимодействия функциональностей в телефонных сетях.
157-167 528
Аннотация
Представлены два направления развития проекта по верификации Си-программ, разрабатываемого в ИСИ СО РАН. Во-первых, аксиоматическая семантика языка C-kernel была расширена семантической разметкой. Метки, выводимые непосредственно исчислением Хоара, соответствуют различным аспектам условий корректности (УК). Эти метки могут быть извлечены из термов и преобразованы в пояснения на естественном языке. Пояснения, понятные обычному пользователю системы верификации, могут быть полезны для понимания УК и локализации ошибок. Во-вторых, было специфицировано подмножество стандартной библиотеки языка Си. Спецификации написаны на языке ACSL и соответствуют модели памяти языка C-light. В работе представлены примеры использования этих двух подходов.
168-180 593
Аннотация
Курс проектирования и анализа алгоритмов является обязательной составляющей учебных программ по информатике всех уровней. В университетах этот курс обязательно включает изучение структур данных, методы проектирования алгоритмов, теорию сложности и т.д. Этот курс знакомит с такими методами проектирования алгоритмов, как жадные алгоритмы, динамическое программирование, метод разделяй и властвуй, метод отката, метод ветвей и границ. Обычно знакомство с этими методами происходит на примерах. Но (как показано в данной статье) они могут быть (полу)формализованы в виде "паттернов", специфицированы условиями частичной и/или тотальной корректности и обоснованы (доказаны) методом Флойда верификации алгоритмов. Такой формализованный подход может привести к новому, более глубокому пониманию этих методов. В статье демонстрируется перспективность такого подхода на примере метода отката и метода ветвей и границ. В частности, мы доказываем, что разработанные шаблоны корректны, если граничное условие - монотонная функция, а решающее условие - антимонотонная функция от множества уже проверенных вершин.
ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)
ISSN 2313-5417 (Online)