TMPA-2013: программа

10.10.2013

О конференции TMPA-2013

Видео репортаж

Открытие конференции TMPA-2013

Верификация

Верификация параллельных программ: современный этап и перспективы

Карпов Юрий Глебович, д.т.н., профессор, заведующий кафедрой «Распределенные вычисления и компьютерные сети» СПбГПУ (о докладчике)

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

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

Современные методы обеспечения высокого качества ПО включают целый арсенал средств, методик и подходов. Хотя основным методом здесь все еще остаются тестирование и отладка программ, в последнее время все более широкое применение получает верификация – формальное доказательство выполнения на формальной модели программной системы формально определенных требований к ее поведению. Прорывным направлением в области формальной верификации стал метод Model checking (проверка модели.

Метод Model checking может быть использован для программных и аппаратных систем, которые представляются модель переходов с конечным числом состояний, поэтому главной проблемой этого метода является «state explosion problem», состоящая в экспоненциальном росте числа состояний системы параллельных программ при увеличении числа взаимодействующих компонент. Разработка «символьных» алгоритмов, основанных на экономных методах представления конечных структур данных, позволило во многом снизить чувствительность этого метода к проблеме “взрыва” числа состояний и существенно увеличить эффективность этого метода верификации. «Символьные» методы верификации были с успехом использованы во многих практических разработках реальных программных систем. Сегодня эта техника применяется как этап технологии во многих крупных фирмах, занимающихся разработкой встроенных систем для критических применений.

Область Model checking остается «горячей» областью информатики, здесь продолжаются интенсивные исследования, возможности этого подхода постоянно расширяются. Недавно группой ведущих ученых в области применения формальных методов в разработке ПО был объявлен амбициозный международный исследовательский проект «Verified Software Initiative», целью которого является доведение теоретических основ, инструментария и элементов технологии верификации до такого состояния, при котором они позволят строить программные системы, вовсе не содержащие ошибок.

Динамическая верификация гибридных систем

Пакулин Н., Институт системного программирования РАН

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

В статье рассмотрены методы верификации моделей гибридных систем и предложена архитектура тестового стенда для проведения динамической верификации гибридной системы.

Верификация программно-конфигурируемых сетей при помощи системы UPPAAL

Подымов В., Попеско У., МГУ имени М.В. Ломоносова

Аннотация. В последние несколько лет активное развитие получили программно-конфигурируемые сети (ПКС) - особый вид компьютерных сетей, в которых все коммутирующие устройства имеют централизованное управление. В статье исследуются задачи формального описания и верификации ПКС. Для описания ПКС используется библиотека элементов UML в редакторе диаграмм Dia. Для верификации ПКС используется программно-инструментальное средство UPPAAL. Основной результат исследований – разработка транслятора, позволяющего по диаграмме сети получить ее модель для верификации в виде сети конечных временных автоматов. Корректность алгоритма трансляции строго обоснована. Проведен ряд экспериментов, которые показывают применимость предложенного метода верификации для проверки свойств поведения ПКС, специфицированных посредством формул темпоральной логики реального времени.

Построение и верификация ПЛК-программ по LTL-спецификации

Кузьмин Е., Рябухин Д., Шипов А., Ярославский государственный университет им. П.Г. Демидова

Аннотация. Описывается подход к программированию логических контроллеров, состоящих в формировании программной LTL-спецификации, последующей ее проверке на корректность средством верификации Cadence SMV и трансляции в код на языке ST.

На пути к технологии разработки средств дедуктивной верификации программ
На пути к технологии разработки средств дедуктивной верификации программ

Ануреев И., Институт систем информатики имени А.П. Ершова

Аннотация. Статья представляет подход к разработке средств дедуктивной верификации программ. Основой подхода является предметно-ориентированный язык для данной предметной области. Сформулированы требования к такому языку и дано обоснование использования языка спецификации предметно-ориентированных систем переходов Atoment в качестве возможного кандидата. Особенности применения подхода и принципы, на которых он основан, проиллюстрированы на простых примерах. На базе подхода предполагается создать технологию разработки средств дедуктивной верификации программ.

Верификация распределенных автоматных программ с использованием инструментального средства Spin
Верификация распределенных автоматных программ с использованием инструментального средства Spin

Лукин М., Шалыто А., СПб НИУ ИТМО

Аннотация. В данной статье рассмотрен комплексный подход к разработке и верификации распределенных автоматных программ, в которых иерархические автоматы могут реализовываться в разных потоках и взаимодействовать друг с другом. Предложен интерактивный подход к верификации распределенных автоматных программ при помощи инструмента Spin, который включает в себя автоматическое построение модели на языке Promela, приведение LTL-формулы в формат, определяемый инструментом Spin и построение контрпримера в терминах автоматов. На основе этого подхода создано инструментальное средство Stater, позволяющее создавать распределенную систему конечных автоматов, генерировать на ее основе программный код на целевых языках программирования и верифицировать ее при помощи верификатора Spin. Автоматы могут быть созданы в инструменте Stater, а также импортированы из Stateflow.

Эффективная универсальная сеть Слепцова
Эффективная универсальная сеть Слепцова

Зайцев Д., Международный гуманитарный университет, Одесса, Украина

Аппаратный трек

Проверка корректности поведения HDL-моделей цифровой аппаратуры на основе динамического сопоставления трасс
Проверка корректности поведения HDL-моделей цифровой аппаратуры на основе динамического сопоставления трасс

Иванников В., Камкин А., Чупилко М., Институт системного программирования Российской академии наук (ИСП РАН)

Аннотация. Проверка корректности поведения HDL-моделей является неотъемлемой частью динамической верификации аппаратуры. Как правило, она основана на сравнении поведения HDL-модели с поведением эталонной модели, разработанной на языке программирования. В процессе верификации на обе модели подается одна и та же последовательность стимулов; реакции перехватываются и сравниваются друг с другом. Из-за абстрактности эталонной модели сопоставление трасс не является тривиальной задачей: порядок событий может не совпадать, а некоторые события одной трассы могут отсутствовать в другой. В работе рассматривается метод динамического сопоставления трасс для моделей аппаратуры разного уровня абстракции. Метод был успешно применен в нескольких промышленных проектах по верификации модулей микропроцессоров.

Использование контрольных точек для верификации SystemC-программ
Использование контрольных точек для верификации SystemC-программ

Шипин А., Соколов В., Чалый Д., Ярославский государственный университет

Аннотация. Верификатор, работающий с использованием метода проверки модели (model checking), должен иметь возможность обхода множества достижимых состояний системы. Для SystemC-моделей генерация этого множества является нетривиальной задачей, так как SystemC представляет собой набор классов, расширяющих язык C++. В результате SystemC-модель системы компилируется в виде исполняемого файла, который позволяет проводить только имитационное моделирование или тестирование. В работе представлен подход, основанный на использовании контрольных точек, реализующий исчерпывающее построение множества достижимых состояний моделируемой системы

Унифицированная высокоуровневая модель программно-аппаратной системы для верификации свойств надежности функционирования
Унифицированная высокоуровневая модель программно-аппаратной системы для верификации свойств надежности функционирования

Френкель С., Захаров В. Н., Ушаков В., Институт проблем информатики РАН, Московский гос. университет им. М.В. Ломоносова

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

Особенности разработки программного обеспечения для Linux-контроллеров

Смирнов М., Олоничев В., Староверов Б., Костромской государственный технологический университет

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

11.10.2013

Тестирование

Технические решения и нетехнические проблемы автоматизации тестирования

Петренко А., д.ф.-м.н., профессор, заведующий отделом «Технологии программирования», ИСПРАН

ISTQB
Об усовершенствовании статистического метода оценки полноты тестов программ и устройств

Басок Б., Гречин А.,Московский государственный технический университет радиотехники, электроники и автоматики

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

Анализ производительности сетевой подсистемы микроядерного окружения Genode
Анализ производительности сетевой подсистемы микроядерного окружения Genode

Сартаков В., Тарасиков А., ksys labs

Аннотация. Микроядерные операционные системы имеют долгую историю развития, однако на сегодняшний день большинство из них остаётся экспериментальными исследовательскими проектами. В данной работе представлен опыт использования микроядра L4 Fiasco.OC и окружения Genode для построения сетевой инфраструктуры, приведен анализ ее производительности, а также рассмотрены архитектурные особенности микроядра и программного окружения, влияющие на пропускную способность сетевой подсистемы.

Подход к верификации корректности миграции данных между СУБД с использованием криптографических хэш-функций

Журавлев М., Полозов В., Санкт-Петербургский Государственный Университет

Аннотация. В данной статье описывается автоматизированный подход к сравнению содержимого баз данных в промышленном проекте по миграции БД из СУБД MS SQL Server 2005 в Oracle 11gR2. Целевая БД должна содержать те же данные, что и исходная с точностью до ограничений, налагаемых используемыми СУБД, и быть функционально эквивалентной. Размер данных в исходной базе составляет порядка 6 терабайт, размер кода - 2.5 миллиона строк кода в хранимых процедурах. Разработан метод сравнения содержимого БД независимый от порядка просмотра записей, использующий коммутативные и криптографические хэш-функции. Показана применимость данного метода для практического использования.

Автоматизация тестирования соответствия протокола безопасности транспортного уровня TLS
Автоматизация тестирования соответствия протокола безопасности транспортного уровня TLS

Никешин А., Пакулин Н., Шнитман В., Институт системного программирования РАН

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

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

Применение технологий OLAP и MapReduce для обработки результатов нагрузочного тестирования

Сенов А., Костромской государственный технологический университет

Аннотация. Современные трейдинговые платформы представляют собой сложные распределённые системы, обслуживающие большое число пользователей по различным протоколам передачи данных. При нагрузочном тестировании таких систем возникает существенный объём информации, которая может быть проанализирована QA-специалистами с целью обнаружения дефектов. Для этого часто требуется выявлять зависимости между значениями показателей, полученными в ходе тестирования путём проведения многофакторного анализа, что при большом объёме данных является трудоёмкой задачей, требующей специализированного ПО, в частности, систем интерактивной аналитической обработки OLAP. В данной статье описывается оригинальный алгоритм многомерного анализа результатов нагрузочного тестирования на стороне клиента. С помощью технологии MapReduce предложенный алгоритм оптимизирован для работы под управлением многоядерных процессоров.

Трейдинговые системы

Особенности инструментов для тестирования, применимых при промышленной эксплуатации трейдинговых систем

Матвеева А., Антонов Н., Иткин И., ООО «Инновационные Трейдинговые Системы», Костромской государственный технологический университет, Exactpro Systems LLC

Aннотация. В статье рассматриваются основные требования к инструментам, разработанным для верификации корректной работы электронных трейдинговых систем с использованием методов большого объема автоматизированного тестирования (НiVAT); анализируется применимость подобных инструментов при промышленной эксплуатации трейдинговых систем.

Тестирование совместимости протокольных подключений клиентов биржевых и брокерских систем

Алексеенко А., Проценко П., Матвеева А., Иткин И., Шаров Д., ООО «Инновационные Трейдинговые Системы», Exactpro Systems LLC

Aннотация. Жизненный цикл разработки биржевого и брокерского программного обеспечения, помимо проверки функциональных и технических характеристик системы, включает в себя обязательный этап интеграционного тестирования, называемый сертификацией клиентов. Этот этап призван обеспечить совместимость систем автоматизированной торговли, подключаемых к бирже или брокеру посредством финансовых протоколов (таких как FIX/FAST, ITCH или специализированные бинарные интерфейсы доступа). В статье представлен оригинальный инструмент, разработанный для проверки совместимости торговых систем. Отличительная особенность разработанного инструмента - унифицированный способ поддержки множества протоколов. Приведены примеры его использования при самостоятельной сертификации участников торгов, а также при масштабных миграциях трейдинговых платформ.

Применение симуляторов рынка ценных бумаг для тестирования систем агрегации и распределения информации о котировках (Ticker Plant)

Буянова О., Булда А, Зверев А., ООО «Инновационные Трейдинговые Системы», Костромской государственный технологический университет, Exactpro Systems LLC

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

Высокопроизводительный генератор нагрузки для тестирования систем автоматизированной торговли

Гурьев Д., Гай М., Иткин И., Терентьев А., ООО «Инновационные Трейдинговые Системы», Саратовский государственный технический университет имени Гагарина Ю.А.

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

Использование MBT-подхода для верификации систем мониторинга и контроля на фондовых биржах

Прядкина Н., Крюков А., Костромской государственный технологический университет

Аннотация. Данная статья описывает проблемы тестирования систем мониторинга и контроля на фондовых биржах (СМКнФБ). На сегодняшний день такие системы представляют собой комплексные программные продукты, реализующие сложные математические алгоритмы и обрабатывающие большой объём данных. Одной из их задач является уменьшение количества ложных срабатываний, что достигается за счёт наиболее полного покрытия при тестировании. В работе определены подходы для адаптации метода тестирования на основе модели (ТнОМ, MBT) к верификации СМКнФБ. Построена структурная модель системы, дано формализованное описание метода в нотации IDEF0. Определены требования к степени абстракции функциональной модели СМКнФБ, необходимой для проведения тестирования.

Тестирование графического интерфейса трейдинговых терминалов в условиях высокочастотной торговли

Бобров И., Зверев А., ООО «Инновационные Трейдинговые Системы»

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

Нешаблонные методы тестирования программного обеспечения для электронных торговых платформ

Круглый стол

12.10.2013

Анализ программ

Математические аспекты задачи обфускации программ

Захаров Владимир Анатольевич, д.ф.-м.н., доцент кафедры МК, зав. лабораторией МПКБ (о докладчике)

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

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

Динамический поиск гонок в Java-программах на основе синхронизационных контрактов

Цителов Д., Трифанов В., Devexperts LLC, СПбГУ

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

Обнаружение дефектов работы с указателями в программах С и С++ с использованием статического анализа и логического вывода

Верт Т., Крикун Т., Глухих М., Санкт-Петербургский государственный политехнический университет, Технический университет Клаусталя

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

Автоматизированный синтез тестов для Java-программ на основе анализа программ и учета контрактов

Андрианова А., Ицыксон В., Санкт-Петербургский государственный политехнический университет

Аннотация. Обеспечение качества создаваемого программного обеспечения является одной из основных проблем программной инженерии. Одним из путей, используемых для повышения качества программ, является автоматизируемый синтез тестов. В статье предлагается технология автоматизированного создания модульных тестов, комбинирующая подходы "белого" и черного" ящиков. При этом для обеспечения покрытия тестами путей программы используется информация, извлекаемая из исходного программы, а для формирования тестовых оракулов и распределения параметров тестов по области определения используются частичные спецификации, заданные в форме контрактов. Разработанный подход реализован в виде инструментального средства, анализирующего программы на языке Java и формирующего тест-кейсы для методов классов в формате JUnit, используя COFOJA для задания контрактов. Тестирование разработанного средства на ряде тестовых примеров показало работоспособность подхода.

Диаграммы классов ООП: формализация и анализ
Диаграммы классов ООП: формализация и анализ

Буй Д., Компан С., Киевский национальный университет имени Тараса Шевченко

Аннотация. В статье приводится короткий сравнительный анализ работ, посвящённых формальным моделям объектно-ориентированного программирования (ООП). Предмет исследования – модель диаграммы классов (соответствующее частично упорядоченное множество). Модель класса (спецификация класса) — пара бинарных функциональных отношений, одна компонента уточняет атрибуты, вторая — методы. Наследование уточняется как включение графиков функций. Над классами вводятся две операции –– пересечение и сочленение. Формальные результаты: структура частично упорядоченного множества классов, свойства операции наложения, в терминах которой вводится операция сочленения: идемпотентность, ассоциативность, критерий коммутативности. Модель диаграммы классов можно использовать для анализа структуры классов, который может помочь для выделения подсистем клонов и оптимизации самой диаграммы.

Как написать хорошую научную статью

Круглый стол