Скачать презентацию

Юрий Карпов

Профессор, доктор технических наук, член Американского Математического общества с 1975 г., эксперт научно-технической сферы Российской Федерации. Научные интересы Ю.Г.Карпова связаны с проблемами формальных моделей параллельных процессов, моделированием и анализом распределенных систем, с верификацией параллельных и распределенных алгоритмов. Был консультантом компании Hewlett-Packard по формальному анализу и верификации протоколов коммуникации. Являлся руководителем нескольких исследовательских проектов, выполнявшихся для Европейских лабораторий HP и для IBM Centre for Advance Studies.

В 1999 г. был приглашенным профессором Института параллельных и высокопроизводительных вычислительных систем Штуттгартского Университета (Германия). Совместно с А.В.Борщевым и В.Рудаковым основал софтверную компанию XJ Technologies и стал ее президентом.
Заведует кафедрой “Распределенные вычисления и компьютерные сети” Санкт-Петербургского политехнического университета с момента её основания в 1995 г. Читает лекции по курсам “Математическая логика и теория алгоритмов”, “Теория автоматов и формальных языков”, “Распределенные алгоритмы и протоколы”, “Верификация параллельных и распределенных программных систем”. Автор более 150 научных и методических публикаций и нескольких книг: “Теория автоматов”, “Теория и технология программирования. Основы построения трансляторов”, “Имитационное моделирование систем. Введение в моделирование с AnyLogic 5”, “Model checking. Верификация параллельных и распределенных программных систем”.

Доклад: На пути к практическому применению верификации в разработке программных систем

Юрий Карпов, Ирина Шошмина

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

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

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

Несмотря на то, что теория и алгоритмы Model checking достаточно подробно разработаны, и даже существуют впечатляющие примеры успешного применения этого метода, до сих пор верификация используется, по классификации Джеффри Мура, только “инноваторами”, “технологическими энтузиастами”, а отчеты об отказах технических систем, произошедших из-за программных ошибок, продолжают ужасать общество. В докладе рассматриваются проблемы, препятствующие внедрению этапа верификации в технологический цикл разработки программ.