Доктор физико-математических наук, профессор
Александр Константинович Петренко

Родился 11 июня 1951 года. Окончил среднюю общеобразовательную школу №7 в г. Химки (1968), факультет прикладной математики Московского института электронного машиностроения (МИЭМ) (1974). В 1983 в ИПМ им. М.В.Келдыша защитил кандидатскую диссертацию на соискание степени кандидата физ.-мат. наук по теме "Инструментальные средства для разработки интерактивных пакетов программ" (научные руководители М.В.Михелев и В.С.Штаркман). В 2003 году в ИСП РАН защитил диссертацию на соискание степени доктора физико-математических наук, тема диссертации "Тестирование на основе формальных спецификаций в процессах разработки программных комплексов", в 2011 году получил ученое звание профессора по специальности. В 2022 году удостоен почетного звания «Заслуженный деятель науки Российской Федерации».

• Технологии верификации и валидации
  • Технология тестирования на основе формальных спецификаций UniTESK
  • Технологии разработки и верификации моделей микропроцессоров
• Моделирование программно-аппаратных систем, язык архитектурного моделирования AADL
  • Проект MASIW Framework
• Формализация интерфейсных стандартов и тестирование их реализаций на соответствие стандартам:
  • Стандарт LSB Core. Проект OLVER (Open Linux VERification)
  • Тестовый набор на совместимость с ARINC-653
• Стандарты качества и надежности программных систем ГОСТ Р 51904-2002 (КТ-178С/DO-178C) и управление требованиями
  • Инструмент для управления требованиями Requality
• Стандарты защиты и безопасности программных систем
  • ГОСТ Р 59453 «Защита информации. Формальная модель управления доступом». Части 1 и 2.
• Операционные системы реального времени (JetOS, БОСРВ)

1. Д. В. Ефремов, В. В. Копач, Е. В. Корныхин, В. В. Кулямин, А. К. Петренко, А. В.Хорошилов, И. В. Щепетков. Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы.- Труды ИСП РАН 33 (6), 2021, 15-26.
2. П. Н. Девянин, Д.В. Ефремов, В. В. Кулямин В. В., Петренко А. К., Хорошилов А. В., Щепетков И. В. Моделирование и верификация политик безопасности управления доступом в операционных системах.- Горячая линия–Телеком, 2019, 216 с.
3. П. Н. Девянин, В. В. Кулямин В. В., Петренко А. К., Хорошилов А. В., Щепетков И. В.Сравнение способов декомпозиции спецификаций на Event-B.- Программирование, 42(4):17-26, 2016.
4. В. В. Кулямин, Е. М. Лаврищева, В. С. Мутилин, А. К. Петренко Верификация и анализ вариабельных операционных систем.- Труды ИСП РАН. Том 28, выпуск 3, 2016 г. Стр. 189-208.
5. И.С. Захаров, М. У. Мандрыкин, В. С. Мутилин, Е. М. Новиков, А. К. Петренко, А. В. Хорошилов. Конфигурируемая система статической верификации модулей ядра операционных систем.- Программирование, №1, 2015, с. 44-67.
6. А. К.Петренко, В. В. Кулямин, А. В. Хорошилов Об интеграции формальных методов в задачах верификации операционных систем.- Труды ИСП РАН. Том 27, выпуск 5, 2015 г. Стр. 175-190.
7. Е. А. Герлиц, В. В. Кулямин, А. В. Максимов, А. К. Петренко, А. В. Хорошилов, А. В. Цыварев. Тестирование операционных систем.- Труды ИСП РАН, том 26, 2014 г. Выпуск 1. Стр. 73-108.
8. Д. В. Буздалов, С. В. Зеленов, Е. В. Корныхин, А. К. Петренко, А. В. Страх, А.А . Угненко, А. В. Хорошилов.Инструментальные средства проектирования систем интегрированной модульной авионики.- Труды ИСП РАН, том 26, 2014 г. Выпуск 1. Стр. 201-230.
9. И. С. Захаров, М. У. Мандрыкин, В. С. Мутилин, Е. М. Новиков, А. К. Петренко, А. В. Хорошилов. “Конфигурируемая система статической верификации модулей ядра операционных систем”.- Труды ИСП , Том 26-2, 2014, с. 5-42.
10. P. Devyanin, A. Khoroshilov, V. Kuliamin, A. Petrenko, I. Shchepetkov. "Formal Verification of OS Security Model with Alloy and Event-B".- In A. Yamine and K.-D. Schewe, eds. Abstract State Machines, Alloy, B, TLA, VDM, and Z, LNCS 8477:309-313, Proceedings of ABZ-2014, Toulouse, France, June 2-6, 2014. ISBN: 978-3-662-43651-6, DOI: 10.1007/978-3-662-43652-3_30.
11. Dirk Beyer and Alexander K. Petrenko. Linux Driver Verification. In T. Margaria and B. Steffen, editors, Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2012, Part II, Heraklion, Crete, October 15-18), LNCS 7610, pages 1-6, 2012. Springer-Verlag, Heidelberg.
12. A. Khoroshilov, I. Koverninskiy, M. Olshanskiy, A. Petrenko, A. Ugnenko. "Model-based Tool Chain For System Design and System Integration of IMA".- In Proceedings of the International Space System Engineering Conference DASIA-2012, pp. 67-71, Dubrovnik, Croatia, May 14-16, 2012.
13. A. Khoroshilov, D. Albitskiy, I. Koverninskiy, M. Olshanskiy, A. Petrenko, A. Ugnenko. "AADL-Based Toolset for IMA System Design and Integration".- SAE Int. J. Aerosp. 5(2):2012, doi:10.4271/2012-01-2146.
14. L. S. Barbosa, A. Cerone, A. K. Petrenko, S. Shaikh. Certification of open-source software: A role for formal methods.-International Journal of Computer Systems Science and Engineering (IJCSSE), Vol 25 No 4 July 2010.
15. A. V. Khoroshilov, V. V. Mutilin, A. K. Petrenko, V. A. Zakharov. Establishing Linux Driver Verification Process.-Proceedings of the PSI 2009, LNCS, Vol. 5947/2010, 165-176.
16. A. K. Petrenko, O. L. Petrenko. Formal Methods and Innovation Economy: Facing New Challenges.- Proceedings of the 6th IEEE International Conference on Software Enginering and Formal Methods, Cape Town, South Africa, 10-14 November 2008.
17. А. К. Петренко, О. Л. Петренко, В. В. Рубанов. Создание открытой образовательной среды на основе открытых проектов.- Тезисы докладов Третьей конференции "Свободное программное обеспечение в высшей школе",Переславль Залесский, февраль 2008, стр. 12-16.
18. В. П. Иванников, А. С. Камкин, А. С. Косачев, В. В. Кулямин, А. К. Петренко. Использование контрактных спецификаций для представления требований при функциональном тестировании аппаратуры.- Программирование, Том.33, № 5, 2007, стр. 47-61.
19. Н. Пакулин, А. К. Петренко, О. Л.Петренко, А. Сортов, А. Хорошилов. Открытые стандарты и новые формы международного сотрудничества.- Труды ИСП РАН, том 13, часть 1, Москва, 2007, стр. 7-30, ISBN 5-89823-026-2.
20. В. П. Иванников, А. К. Петренко. Задачи верификации ОС Linux в контексте ее использования в государственном секторе.- Труды ИСП РАН, том 10, Москва, 2006, стр. 9-14, ISBN 5-89823-026-2/
21. A. Grinevich, A. Khoroshilov, V. Kuliamin, D. Markovtsev, A. Petrenko, V. Rubanov. Formal Methods in Industrial Software Standards Enforcement.- Procs. of PSI'2006, Novosibirsk, Russia, LNCS 4378:459-469, 2006
22. S. Zelenov, D. Silakov, A. K. Petrenko, M. Conrad, I. Fey. Automatic Test Generation for Model-Based code Generators.- IEEE ISoLA 2006 Second Intern.Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Paphos, Cyprus, 2006, pp. 68-75.
23. V. V. Kuliamin, N. Pakulin, A. K. Petrenko. Extended Design-by-Contract Approach to Specification and Conformance Testing of Distributed Software.- Proc. of 9-th World Multi-Conference on Systems, Cybernetics, and Informatics, Orlando, USA, July 2005, v. VII. Model Based Development and Testing, pp. 65-70.
24. В. В.Кулямин, И. Б.Бурдонов, А. С. Косачев, А. К. Петренко. Подход UniTesK к разработке тестов.-Программирование, том 29, №6, 2003, стр. 25-43.
25. Е. Н. Бритвина, С. Г. Грошев, А. Монахов, А. К. Петренко, О. Л. Петренко. Тестирование на основе моделей.-Открытые системы, Москва, № 9, 2003, стр. 41-47
26. С. В. Зеленов, С. А. Зеленова, А. С. Косачев, А. К. Петренко. Генерация тестов для компиляторов и других текстовых процессоров.-"Программирование", Москва, 2003, том. 29, N 3.
27. A. K. Petrenko. Specification Based Testing: Towards Practice. Perspectives of System Informatics.-LNCS, No.2244, 2001, pp. 287-300.
28. А. К. Петренко, Е.А.Кузьменкова Формальная спецификация программ на языке RSL (методическое пособие по практикуму). МГУ им. М.В.Ломоносова, Москва, 1999.
29. I. B. Burdonov, A.S. Kossatchev, A. K. Petrenko, D. Galter KVEST: Automated Generation of Test Suites from Formal Specifications.- Proceedings of Formal Method Congress, Toulouse, France, 1999, LNCS, No. 1708, pp.608-621.
30. А. К. Петренко. Технология программирования.- Сборник "Современное состояние и тенденции развития информационных технологий в России", Миннауки, Научный совет по ГНТП "Информатизация России", 1995 г., стр.88-108.
31. I. Burdonov, A. Kossatchev, S. Cheng, H. Wong. Formal Specification and Verification of SOS Kernel.- BNR/NORTEL Design Forum, June 1996.
32. А. К. Петренко. Методы отладки и мониторинга параллельных программ. Програмирование,3,1994.
33. V. A. Krukov, K. B. Fedorov, A. K. Petrenko, Yu. V. Trunov. GRAPHIT-graphic integrated environment for real-time system development.- Procs. of the Intern. Conf. "Real-Time Data RTD-94", Dubna, June 1994.
34. В. А. Крюков, А. В. Максимов, А. К. Петренко, Т. А. Полилова. Иерархическое конфигурационное управление.- Програмирование,2,1994.
35. А. К. Петренко, Спецификация тестов на основе описания трасс.- Программирование, 1, 1993.
36. А. К. Петренко, М. В. Борисова, Т. А. Морозова, Т. А. Чацкина. Тестирование компиляторов на основе формальной модели языка.- Препринт ИПМ, N 45, 1992.
37. А. К. Петренко. Венский метод разработки программ - VDM. Неформальное введение.- Программирование, N 6, 1990.
38. А. К. Петренко. Проблемы построения базы данных для интегрированных сред.- В кн.: IV Всесоюзная науч. конференция Системы баз данных и знаний НПО Центрпрограммсистем,Калинин, 1990.
39. В. А. Крюков, А. К. Петренко, М. Р. Шура-Бура. Транслятор в системе автоматизации разработки.- В сб.: Методы трансляции и конструирован. программ. Тез. Всес. конференции, Новосибирск, 1988.
40. А. К. Петренко. Система Мимоза. Концепции и возможности. Препринт ИПМ АН СССР, N 4 1983.
41. А. К. Петренко. Интерактивная система общения с задачей - Мимоза.- В сб.:Проблемы проектирования и применения дискретных систем в управл. Тезисы докл. Минск, 1977
42. А. К. Петренко, О. Л. Петренко. Машина Беббиджа и возникновение программирования.- Истор.-математические исследования.- Вып. XXIV. М."Наука 1976.
43. А. К. Петренко, С. А. Усов. Диалоговый монитор - Димон. Запуск задач в пакет.- Препринт ИПМ АН СССР,N 69 1975.

• Российский Фонд Фундаментальных Исследований (РФФИ)
• Минобрнауки РФ
• НИИСИ РАН
• ГосНИИАС
• Nortel Networks
• 6-я и 7-я Европейские Рамочные Программы (Framework Programs)
• Microsoft Research
• Intel
• Daimler Chrysler Research
• The Linux Foundation
• HUAWEI

• Развитие инфраструктуры поддержки стандарта Linux Standard Base (LSB) (2006-2014)
• Тестирование программных систем компании Вымпелком (2003-2013)
• Тестирование операционных систем реального времени ОС2000 и ОС3000 (2005-2020)
• Тестирование микропроцессоров
• Комплекс инструментальных средств для проектирования и верификации Интегрированной Модульной Авионики (ИМА)
• Разработка операционной системы реального времени JetOS
• Разработка операционной системы реального времени БОСРВ

• Международный семинар по тестированию на основе моделей (Model Based Testing - MBT) 2004-2015 годы.
• Весенняя Spring Young Researchers Colloquium on Software Engineering, SyrcoSE с 2007 г. по настоящее время.
• Конференции OS Day, 2014, 2015.
• Перспективы системной информатики (Perspectives of System Informatics - PSI) 2017.
• TOOLS 50+1: Software Technology: Methods and Tools, Innopolis, 2019 .
• Конференции "Актуальные проблемы системной и программной инженерии" - АПСПИ, 2015-2021.