31.10 «Разработка ПО: Банки», курсы « Продажи софтверных продуктов и услуг», «CMMI» и «Польза от пользователя», 31.10–1.11 «Cкрам-мастер»
SECR 2011 завершил работу. Получить информацию о текущей конференции можно на www.secr.ru.

Юрий Карпов


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

 

 
Юрий Глебович Карпов
Юрий Карпов

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

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

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

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

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

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

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

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

 



Комментарии


Оставить комментарий

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>

© CEE-SECR 2011 • Email: contact@secr.ru
Proudly powered by WordPress. • Hosted by Hosting Community