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

14.11.2014

Вести Кострома о TMPA-2014

Московская биржа

Актуальные проблемы разработки эффективных параллельных алгоритмов и структур данных

Виталий Трифанов, Дмитрий Цителов, Devexperts LLC, Санкт-Петербург

Актуальные проблемы разработки эффективных параллельных алгоритмов и структур данных. Основное направление деятельности компании Devexperts - разработка высоконагруженного ПО для комплексной автоматизации брокерской, биржевой и финансовой деятельности. Специфика отрасли диктует необходимость разработки и верификации реализаций lock-free/wait-free алгоритмов и структур данных, которые эффективно используют многопроцессорные системы с общей памятью, доказательства корректности их работы. В последнем десятилетии данное направление получило особую актуальность, и в нём существует ряд слабо изученных тем. Кроме того, зачастую теоретические разработки не подкреплены практической реализацией. Мы расскажем об основных направлениях исследований, актуальных для нас, и затронем тему организации взаимовыгодного сотрудничества с ВУЗами на стыке науки и бизнеса.

Новая биржевая платформа НП РТС: задачи, архитектура и управление рисками

Михаил Вьюгин, Некоммерческое партнерство развития финансового рынка РТС

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

Introduction into Fault-tolerant Distributed Algorithms and their Modeling (Part 1)

Josef Widder, Vienna University of Technology (о докладчике)

Fault-tolerant distributed algorithms provide a system designer with a mechanism for constructing reliable computing systems. In this talk, we will introduce basic notions such as timing assumptions, fault assumptions, and classic problems in this area. By reviewing classic paper & pencil correctness arguments, we motivate the use of automated verification methods such as model checking.
The first step towards automated verification is adequate modeling. Thus, in the second part of the talk, we explain how to encode the semantics of fault-tolerant distributed algorithms in Promela, the input language of the Spin model checker.

Introduction into Fault-tolerant Distributed Algorithms and their Modeling (Part 2)

Josef Widder, Vienna University of Technology (о докладчике)

A runtime verification system for Software Defined Networks (RU)

Виктор Алтухов, Евгений Чемеритский, Владислав Подымов, Владимир Захаров, МГУ им. М.В. Ломоносова, ЦПИКС, Москва

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

Михаил Никитинский, Дмитрий Чалый, ЯрГУ им. П.Г. Демидова, ООО «Энергия-Инфо», Ярославль

Балансировка сетевого трафика является одним из важных элементов построения и организации отказоустойчивости в коммуникационных сетях. На данный момент существует множество алгоритмов балансировки, как для стандартных подходов организации сетей, так и для программно-конфигурируемых сетей (ПКС). Нами разрабатывается асимметричный транспортный протокол, одним из его свойств является возможность использовать метод anycast для параллельной связи с несколькими серверами. В данной статье будут рассмотрены возможные варианты применения семейства асимметричных транспортных протоколов для улучшения балансировки в ПКС.

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

Дмитрий Чалый, ЯрГУ им. П.Г. Демидова, Ярославль

Транспортные протоколы, в особенности протокол TCP (Transmission Control Protocol), являются ключевым компонентом архитектуры TCP/IP, используемой в современных коммуникационных сетях. Разработка и исследование свойств новых транспортных протоколов требует умения решать широкий спектр задач в области их моделирования, верификации и проведении анализа производительности. Однако зачастую в рамках этих исследований еще одна задача остается нерассмотренной — организация процесса исследований таким образом, чтобы они могли быть автоматизированно, а в идеале автоматически, возпроизведены другими учеными. В этой статье рассматриваются подходы и методики, которые позволяют обеспечить воспроизводимость результатов исследований (reproducible research) в области коммуникационных протоколов

Профилирование систем реального времени

Денис Дерюгин, СПбГУ, Санкт-Петербург

В данной статье анализируются особенности профилирования программного обеспечения для систем реального времени. Рассматриваются специфичные для области проблемы: многозадачность, точность замеров, кросс-платформенность, необходимость замерять время работы уровней пользователя и ядра одновременно (”сквозное” профилирование), а также ряд других. Производится сравнение различных подходов к профилированию систем реального времени. Приведены аргументы в пользу инструментирования как эффективного метода для проведения “сквозного” профилирования.

Совместное применение методов Model driven developing и Model based checking

Сергей Старолетов, АлтГТУ, Барнаул

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

Автоматизация тестирования системы резервирования

Вадим Жердер, Татьяна Ульянина, ОАО Московская биржа, НИЯУ МИФИ, Москва

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

Система контроля рисков в высоконагруженных биржевых и брокерских системах и её тестирование

Алена Булда, Максим Рудовский, Алексей Зверев, Exactpro Systems, Кострома, Москва

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

Trading Day Logs Replay Limitations and Test Tools Applicability

Павел Проценко, Анна Христенок, Андрей Алексеенко, Анна-Мария Лукина, Иосиф Иткин, Татьяна Павлюк, Exactpro Systems, Лондон, Кострома, Москва, Обнинск

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

Всеволод Брекелов,Илья Барыгин, Егор Борисов, Devexperts LLC, Санкт-Петербург

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

Моделирование тестовых сценариев поведения участников биржевой торговли

Елена Герасимова, Ростислав Яворский, ВШЭ, Москва

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

Как мы тестируем в Exactpro

Иосиф Иткин, Exactpro Systems

Компания Exactpro Systems создана в конце 2009 года. Доклад рассказывает:

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

О моделировании согласованного поведения ПЛК-датчиков

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

Статья продолжает цикл работ, посвященный разработке подхода к построению и верификации «дискретных» программ логических контроллеров (ПЛК), обеспечивающего возможность анализа их корректности с помощью метода проверки модели (model checking), — программирование и верификация по LTL-спецификации.При верификации ПЛК-программы методом проверки модели возникает необходимость в построении ее конечной модели. При этом для успешной проверки соответствия модели требуемым программным свойствам важно учитывать то, что далеко не все комбинации входных сигналов от датчиков могут встречаться в действительности при работе ПЛК с объектом управления.Этот факт требует более внимательного отношения к построению модели программы ПЛК. В статье предлагается описывать согласованное поведение датчиков с помощью трех групп LTL-формул, которые при проверки справедливости программных свойств будут оказывать влияние на программную модель, приближая ее к реальному поведению исходной ПЛК программы.Идея LTL-требований демонстрируется на примере. Программа ПЛК представляет собой описание реакций на входные сигналы от датчиков,переключателей и кнопок. Предложенный подход к моделированию согласованного поведения ПЛК-датчиков при построении модели программы ПЛК позволяет сосредоточиться на моделировании именно этих реакций по тексту программы без внедрения в код модели дополнительных конструкций, призванных отразить реалистичное поведение датчиков. Согласованное поведение датчиков учитывается лишь на стадии проверки соответствия программной модели требуемым свойствам, т. е. доказательство выполнимости свойств для построенной модели происходит с условием,что рассматриваемая модель содержит только те исполнения исходной программы, которые отвечают требованиям согласованного поведения датчиков.

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

Василий Сартаков, Николай Голиков, ksys labs, Одинцово

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

Автоматизированное тестирование инженерных приложений посредством AutoIt

Алёна Киселёва, ИАП РАН, Москва

Анализ покрытия UCM-модели тестовыми сценариями

Игорь Никифоров, Павел Дробинцев, Всеволод Котляров, Никита Воинов, СПбПУ, Санкт-Петербург

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

Генерация тестового набора на основе модели потока управления

Павел Дробинцев, Всеволод Котляров, Игорь Никифоров Никита Воинов, СПбПУ, Санкт-Петербург

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

15.11.2014

Обобщённый Табличный LL-анализ

Анастасия Рагозина, Семён Григорьев, СПбГУ, JetBrains, Санкт-Петербург

Синтаксический анализ является важным шагом анализа любой системы, поскольку позволяет создать её структурное представление, которое используется в дальнейшем. Для работы с неоднозначными грамматиками используются обобщенные алгоритмы синтаксического анализа (GLR, GLL). Для работы со встроенными языками используется абстрактный синтаксический анализ, основанный на классическом табличном синтаксическом анализе. В данной статье описан подход к созданию табличного GLL-анализатора, который в дальнейшем будет использоваться для получения абстрактного анализатора.

Extended High-Level C-Compatible Memory Model with Limited Low-Level Pointer Cast Support for Jessie Intermediate Language

Михаил Мандрыкин, Алексей Хорошилов, ИСП РАН, Москва

Alias Calculus for a Simple Imperative Language with Decidable Pointer Arithmetic

Николай Шилов, Александр Воронцов, Айжан Сатекбаева, НГУ, Новосибирск, Назарбаев Университет, ЕНУ им.Л.Н.Гумилёва, Казахстан

Метод построения расширенных конечных автоматов по HDL-описанию на основе статического анализа кода

Сергей Смолов, Александр Камкин, ИСП РАН, Москва

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

Анализ AADL моделей с помощью графического представления

Александр Страх, ИСП РАН, Москва

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

Lightweight Static Analysis for Data Race Detection in Operating System Kernels

Павел Андрианов, Алексей Хорошилов, Вадим Мутилин, ИСП РАН, Москва

Статический анализ управления транзакциями в приложениях для платформы Java EE

Иван Грачев, Андрей Соловьев, Кафедра ИСПИ, ВлГУ им. А.Г. и Н.Г. Столетовых, Владимир

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

Parametrized Model Checking of Fault-tolerant Distributed Algorithms by Abstraction (Part 1)

Igor Konnov, Vienna University of Technology

Parametrized Model Checking of Fault-tolerant Distributed Algorithms by Abstraction (Part 2)

Igor Konnov, Vienna University of Technology

Agile-тестировщик: профессионал или ремесленник?

Андрей Конушин, RSTQB, Владимир

Гибкое тестирование - относительно новый подход в тестировании ПО, который следует принципам гибкой (agile) разработки ПО, описанным в документе ""Manifesto for Agile Software Development"". Тестировщик в проектах, основанных на принципах agile, работает иначе, чем в рамках традиционной проектной методологии. Тестировщики должны понимать ценности и принципы таких проектов, как коммуницировать в общекомандном подходе с разработчиками и представителями заказчика. Гибкоe тестированиe как подход к проектам представляет собой тему, вызывающую весьма большое количество сомнений, а следовательно, и достаточно обширную область для изучения и обучения. Модуль Agile Extension системы ISTQB Certified Tester дает тестировщикам знания, необходимые для того, чтобы стать частью команды в гибком тестировании и достигать высоких результатов.

Технологии автоматизированной разработки и верификации программ в аэрокосмической отрасли

Андрей Тюгашев, СГАУ, Самара

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

Андрей Миронов, Сергей Френкель, ИПИ РАН, Москва

Рассматривается задача редукции вероятностных систем переходов (ВСП) с целью понижения сложности верификации таких систем. Верификация ВСП заключается в вычислении истинных значений формул вероятностной темпоральной логики (PCTL, Probabilistic Computational Tree Logic) в начальных состояниях ВСП. Введено понятие эквивалентности состояний ВСП, и описан алгоритм удаления эквивалентных состояний, в результате работы которого получается такая ВСП, у которой все свойства, выражаемые формулами логики PCTL, совпадают со свойствами исходной ВСП.

Верификация 800 автоматных программ, построенных при помощи генетического программирования

Михаил Лукин, Максим Буздалов, Анатолий Шалыто, ИТМО, Санкт-Петербург

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

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

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

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

Оптимизация автоматных программ методом трансформации требований

Владимир Шелехов, Институт систем информатики им А.П. Ершова СО РАН, Новосибирск

Технология автоматного программирования ориентирована на разработку простых, надежных и эффективных программ для класса реактивных систем. Автоматная программа реализует конечный автомат в виде гиперграфа управляющих состояний. В качестве языка спецификаций автоматных программ предлагается язык продукций, применяемый для описания сценариев использования (use case) – одного из видов функциональных требований. Этот простой язык с высокой степенью декларативности. Спецификация программы компактна и легко транслируется в эффективную программу. Построение эффективных автоматных программ реализуется применением набора оптимизирующих трансформаций программы, определяемой в виде набора правил (продукций). Данный метод иллюстрируется на примере сложного протокола передачи данных ATM Adaptation Layer уровня Type 2 AAL.

Система дедуктивной верификации предикатных программ

Михаил Чушкин, Институт систем информатики им А.П. Ершова СО РАН, Новосибирск

На базе аппарата формальной логической семантики разработан новый метод генерации формул тотальной корректности рекурсивных программ без циклов и указателей. Для языка предикатного программирования реализована система дедуктивной верификации, генерирующая формулы корректности. Разработана система правил для упрощения генерации формул корректности. Условия совместимости типов, которые трудно проверить при трансляции с языка предикатного программирования добавляются к формулам тотальной корректности. Сгенерированные формулы поступают в SMT-решатель CVC3. Оставшиеся недоказанные формулы оформляются в виде теорий для доказательства в системе PVS. Система верификации успешно использовалась магистрантами НГУ для дедуктивной верификации программ в рамках заданий по курсу “Формальные методы в описании языков и систем программирования”.

Сервисная робототехника в науке и образовании

Яков Кириленко, CyberTech, Санкт-Петербург