Александр Камкин

Александр Камкин – к.ф.-м.н., старший научный сотрудник Института системного программирования РАН. Область научных интересов: спецификация и верификация цифровой аппаратуры, статический и динамический анализ HDL-описаний, генерация тестов для микропроцессоров.

Oleksandr Letichevskyy

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

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

На этапе дизайна модели рассматривается доказательство аннотаций, соответствие исходным требованиям, сохранение свойств а также дедуктивное тестирование модели и доказательное моделирование.

Рассматривается также дедуктивное тестирование С\С++ кода, как особая техника тестирования достигающая максимальное покрытие сценариев поведение системы.

Докладчик: Летичевский Александр Александрович - к.ф.-м.н., ст.научн.сотр. Института кибернетики имени В.М. Глушкова (Киев). Области интересов - символьное и доказательное моделирование, техника инвариантов, техники тестирования спецификаций, автоматизация доказательств, индуктивный вывод, верификация формальных спецификаций.

Александр Леонидович Александров

Докладчик: Александр Леонидович Александров – к.ф.-м.н., ст. научн. сотр., доцент, руководитель группы в компании Luxoft. Окончил мехмат МГУ и аспирантуру МГУ. После окончания МГУ в 1970 году работал в Вычислительном центре МГУ и на факультете ВМК МГУ до 1999 года. Занимался разработкой стандартов языков программирования, компиляторов, разработкой и эксплуатацией информационных систем, тестированием и документированием, поставкой проекционного оборудования, управлением проектами. Затем перешёл в компанию Luxoft. Эксперт по управлению качеством, инструктор Luxoft Training. Область научных интересов – тестирование ПО, анализ требований к программному обеспечению, совершенствование процессов программной инженерии, обучение, консалтинг.

Балашов Василий Викторович

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

Докладчик: Балашов Василий Викторович, к.ф.-м.н., м.н.с. ЛВК МГУ имени М.В. Ломоносова. С 2001 года участвует в научно-технических работах по созданию технологий и инструментальных средств отработки ПО авиационных бортовых вычислительных систем.

Жданов Александр Аркадьевич

Жданов Александр Аркадьевич, профессор, д.ф.-м.н., главный научный сотрудник ОАО «Институт точной механики и вычислительной техники имени С.А. Лебедева РАН», автор монографии «Автономный искусственный интеллект» расскажет о своем понимании алгоритма биологической системы управления, имплементированной во всех без исключения живых организмах, по результатам своих многолетних исследований в области кибернетики, теории управления, теоретических основ информатики, нейрофизиологии. Будут рассмотрены также способы и инструментарий разработки такого рода программ, примеры прототипов практических систем.

Avalanche - это открытая разработка ИСП РАН, совместно с Samsung. Avalanche использует возможности динамической инструментации программы, предоставляемые Valgrind, для сбора и анализа трассы выполнения программы. Результатом такого анализа становится либо набор входных данных, на которых в программе возникает ошибка, либо набор новых тестовых данных, позволяющий обойти ранее не выполнявшиеся, и соответственно, еще не проверенные, фрагменты программы. Таким образом, имея единственный набор тестовых данных, Avalanche реализует итеративный динамический анализ, при котором программа многократно выполняется на различных, автоматически генерированных тестовых данных, при этом каждый новый запуск увеличивает покрытие кода программы такими тестами.

Докладчик: Сидоров Денис Владимирович, выпускник факультета ВМК МГУ 1999 года, сотрудник ИСП РАН с 1998 года, ведущий разработчик отдела системного программирования (группа анализа программ). Проекты: Klocwork Insight (система обратной инженерии, архитектурного и статического анализа), Avalanche. Области научных интересов: статический и динамический анализ программ, автоматический поиск ошибок в программах, автоматическая трансформация программ.

web: http://ispras.ru/ru/sp/contacts.php