Биография

ПЕТРЕНКО Александр Константинович (11.06.1951, г. Химки, Московской обл.) — заведующий отделом Технологий программирования Института системного программирования им. В. П. Иванникова Российской академии наук (ИСП РАН), профессор кафедры Системного программирования Факультета вычислительной математики и кибернетики Московского государственного университета им. М. В. Ломоносова (ВМК МГУ), профессор, Академический руководитель образовательной программы "Системное программирование" на Факультете компьютерных наук НИУ Высшая школа экономики (ФКН ВШЭ). В 2022 году удостоен почетного звания "Заслуженный деятель науки Российской Федерации".

Окончил среднюю общеобразовательную школу № 7 в г. Химки (1968) и Факультет прикладной математики (ФПМ) Московского института электронного машиностроения – МИЭМ (1974).

Кандидат физ.-мат. наук (1983), тема диссертации: «Инструментальные средства для разработки интерактивных пакетов программ» (научный руководитель В.С. Штаркман). Доктор физ.-мат. наук (2003), тема диссертации «Тестирование на основе формальных спецификаций в процессах разработки программных комплексов». Ученое звание профессор (2008). Член IEEE Computer Society, член ACM, почетный член индийского Компьютерного общества, член Общества истории информационных технологий, член редколлегии журнала «Программирование», организатор Международного научного семинара по тестированию на основе моделей (Model Based Testing - MBT) (2005-2015) и Коллоквиума для молодых ученых по программной инженерии (Spring Young Researchers Colloquium on Software Engineering - SyrcoSE) (2007-2023). С 1974 по 2002 гг. работал в Институте прикладной математики им. М.В. Келдыша РАН (стажер-исследователь, научный сотрудник, заведующий сектором); с 1994 г. работает в ИСП РАН, с 2004 года в должности заведующего отделом.

Участвовал в создании и внедрении одной из первых реализаций удаленной подготовки и запуска задач системе "Димон", которая эксплуатировалась более чем в 50 организациях СССР (1974-1982), в разработке системы программирования в рамках программы "Буран" (1983-1992). С 1994 года является научным руководитель работ по созданию средств верификации ответственного программного обеспечения и микропроцессоров на основе использования формальных методов и по разработке операционных систем реального времени для аэрокосмической техники. С 2007 года научный руководитель Центра верификации ОС Linux.

Основные направления исследований: формальные методы спецификаци и верификации программ и микропроцессоров, методы моделирования программно-аппаратных систем, процессы анализа и обеспечения качества ПО, свободное программное обеспечение и открытые стандарты, стандарты в области надежности и безопасности программных систем. Был участником и руководил следующими программными проектами:
• 1993-1983 – ЛИСП/МИМОЗА – Инструментальная система для разработки интерактивных пакетов прикладных программ,
• 1994-1983 – ДИМОН – Диалоговый монитор для редактирования и удаленного запуска задач,
• 1989-1993 – СиПРОЛ/ГРАФИТ – Система программирования для многоразовой космической системы «Буран»,
• 1994-1999 – Серий проектов с компанией Nortel Networks, технология KVEST – технология генерации тестов на основе контрактных спецификаций программного интерфейса,
• 1999-2007 – Серия работ по технологии тестирования на основе формальных моделей специфицированных на расширениях традиционных языков программирования (UniTESK).
• 2005-2007 – Проект OLVER – при помощи UniTESK разработан один из самых крупных пакетов формальных спецификаций интерфейсных стандартов – Linux Standard Base – LSB (более 1500 интерфейсов), включающего в себя основную часть стандарта POSIX,
• 2007-2013 – Система тестирования для стандарта ARINC-653 (программный интерфейс ОС реального времени).
• 2005–н.в. – Тестирование HDL моделей микропроцессоров для архитектур, разработаны специализированные варианты инструментов UniTESK C++TESK и MicroTESK.
• 2006-2013 – Проект LDV – разработка системы верификации драйверов ОС Linux при помощи методов предикатных абстракций, уточнения абстракций на основе контрпримеров (CEGAR) и других перспективных методов верификации программ.
• 2009-н.в. – Технологии создания систем интегрированной модульной авионики для гражданских воздушных судов, задачи архитектурного моделирования, управления требованиями, верификации и поддержки сертификации.
• 2013-н.в. – Развитие и применение технологий инструментов для глубокой верификации критических компонентов программ для компаний РусБИТех (Astra Linux), Базальт СПО (ALT Linux), ГосНИИАС, Лаборатория Касперского.
• 2017-н.в. – Технологии разработки операционных систем реального времени, отвечающих повышенным требованиям по надежности (DO-178С.КТ-178С).
• 2019-н.в. – Разработка стандартов и регламентов в области обеспечения надежности и защищенности программных систем.

А.К. Петренко опубликовал свыше 100 научных работ, в том числе:

  1. Машина Беббиджа и возникновение программирования // Историко-математические исследования, 1979, № 24, c. 340–360, 389 (соавтор О.Л.Петренко);
  2. KVEST: Automated Generation of Test Suites from Formal Specifications // Proceedings of World Congress of Formal Methods — Toulouse, France, LNCS, 1999, N 1708, pp. 608–621 (соавторы: I. B. Burdonov, A. S. Kossatchev, S. Cheng, D. Galter);
  3. Specification Based Testing: Towards Practice // Proceedings of VI Ershov Memorial Conference 2001 — LNCS, 2001, N2244, pp. 287–300;
  4. Подход UniTesK к разработке тестов // Программирование, 2003, т. 29, № 6 (соавторы: В.В.Кулямин, А.С.Косачев, И.Б.Бурдонов);
  5. Использование контрактных спецификаций для представления требований при функциональном тестировании аппаратуры // Программирование, Том.33, № 5, 2007, стр. 47-61, (соавторы: В. П. Иванников, А. С. Камкин, В. В. Кулямин, А. С. Косачев,);
  6. AADL-based toolset for IMA system design and integration // SAE International Journal of Aerospace 5 (2), 2012, 294 (соавторы: A. Khoroshilov, D. Albitskiy, I. Koverninskiy, M. Olshanskiy);
  7. Об интеграции формальных методов в задачах верификации операционных систем // Труды ИСП РАН 27 (5), 2015, 175-190 (соавторы: В. В. Кулямин, А. В. Хорошилов);
  8. О представлении модельного времени при помощи механизмов функционального программирования // Труды ИСП РАН 30 (6), 2018, 341-366 (соавторы: Д. В. Буздалов, А. В. Хорошилов);
  9. Моделирование и верификация политик безопасности управления доступом в операционных системах // Горячая линия–Телеком, 2019, 216 с. (соавторы: П. Н. Девянин, Д. В. Ефремов, В. В. Кулямин, А. В. Хорошилов, И. В. Щепетков);
  10. Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы // Труды ИСП РАН 33 (6), 2021, 15-26 (соавторы: Д. В. Ефремов, В. В. Копач, Е. В. Корныхин, В. В. Кулямин, А. В.Хорошилов, И. В. Щепетков).

Под его руководством защищено 13 диссертаций на степень кандидата физико-математических и технических наук.

Электронный адрес: petrenko@ispras.ru

Назад