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

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

• Технологии верификации и валидации
  • Отдел Технологий программирования ИСП РАН
  • Технология тестирования на основе формальных спецификаций UniTESK
  • Технологии разработки и верификации моделей микропроцессоров
• Моделирование программно-аппаратных систем
  • Проект MASIW Framework
• Формализация интерфейсных стандартов
  • Проект OLVER (Open Linux VERification)
• Свободное ПО, открытые стандарты
  • Статический анализ драйверов ОС Linux
  • Свободные инструменты отдела

1. Девянин П. Н., Кулямин В. В., Петренко А. К., Хорошилов А. В., Щепетков И. В. Сравнение способов декомпозиции спецификаций на Event-B. Программирование, 42(4):17-26, 2016
2. В.В. Кулямин, Е.М. Лаврищева, В.С. Мутилин, А.К. Петренко Верификация и анализ вариабельных операционных систем Труды Института системного программирования РАН. Том 28, выпуск 3, 2016 г. Стр. 189-208.
3. И.С. Захаров, М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.К. Петренко, А.В. Хорошилов. Конфигурируемая система статической верификации модулей ядра операционных систем. Программирование, №1, 2015, с. 44-67.
4. А.К.Петренко, В.В.Кулямин, А.В.Хорошилов Об интеграции формальных методов в задачах верификации операционных систем Труды Института системного программирования РАН. Том 27, выпуск 5, 2015 г. Стр. 175-190.
5. Е.А. Герлиц, В.В. Кулямин, А.В. Максимов, А.К. Петренко, А.В. Хорошилов, А.В. Цыварев. Тестирование операционных систем. Труды Института системного программирования РАН, том 26, 2014 г. Выпуск 1. Стр. 73-108.
6. Д.В. Буздалов, С.В. Зеленов, Е.В. Корныхин, А.К. Петренко, А.В. Страх, А.А. Угненко, А.В. Хорошилов.Инструментальные средства проектирования систем интегрированной модульной авионики. Труды Института системного программирования РАН, том 26, 2014 г. Выпуск 1. Стр. 201-230.
7. И.С. Захаров, М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.К. Петренко, А.В. Хорошилов. “Конфигурируемая система статической верификации модулей ядра операционных систем”. Труды Института Системного Программирования, Том 26-2, 2014, с. 5-42.
8. Petr Devyanin, Alexey Khoroshilov, Victor Kuliamin, Alexander Petrenko, Ilya 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.
9. 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.
10. 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.
11. Khoroshilov, A., Albitskiy, D., Koverninskiy, I., Olshanskiy, M., Petrenko, A., Ugnenko, A., "AADL-Based Toolset for IMA System Design and Integration", SAE Int. J. Aerosp. 5(2):2012, doi:10.4271/2012-01-2146.
12. 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.
13. 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.
14. Model-Based Testing // Editors of proceddings: Yu.Gurevich, B.Finkbeiner, A.K.Petrenko. Electronic Note in Theoretical Computer Science, 2009, 115 pages.
15. 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.
16. Петренко А.К., О.Л.Петренко, В.В.Рубанов. Создание открытой образовательной среды на основе открытых проектов // Тезисы докладов Третьей конференции "Свободное программное обеспечение в высшей школе",Переславль Залесский, февраль 2008, стр. 12-16.
17. В.П.Иванников, А.С.Камкин, А.С.Косачев, В.В.Кулямин, Петренко А.К. Использование контрактных спецификаций для представления требований при функциональном тестировании аппаратуры // Программирование, Том.33, № 5, 2007, стр. 47-61.
18. Н.Пакулин, А.К. Петренко, О.Петренко, А.Сортов, А.Хорошилов. Открытые стандарты и новые формы международного сотрудничества // Труды ИСП РАН, том 13, часть 1, Москва, 2007, стр. 7-30, ISBN 5-89823-026-2.
19. В.Кулямин, В.Рубанов, А.Хорошилов, А.К.Петренко. Формализация интерфейсных стандартов и автоматическое построение тестов соответствия // Информационные технологии, № 8, 2007, стр. 2-7.
20. В.П.Иванников, Петренко А.К. Задачи верификации ОС Linux в контексте ее использования в государственном секторе // Труды ИСП РАН, том 10, Москва, 2006, стр. 9-14, ISBN 5-89823-026-2/
21. A.Grinevich, A.Khoroshilov, V.Kuliamin, D.Markovtsev, V.Rubanov Formal Methods in Industrial Software Standards Enforcement // 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. V.V.Kuliamin, N.Pakulin, A.K.Petrenko. Practical Approach to Specification and Conformance Testing of Distributed Network Applications // Lecture Notes in Computer Science Volume 3694 / 2005, Title: Service Availability: Second International Service Availability Symposium, ISAS 2005, Berlin, Germany.
25. V.V.Kuliamin, A.K.Petrenko. Applying Model Based Testing in Different Contexts // Proceedings of Seminar on Perspectives of Model-based Testing, Dagstuhl, Germany, September 2004.
26. Kuliamin V., Kossatchev A., Bourdonov I., A.K.Petrenko. UniTesK: Model Based Testing in Industrial Practice // Proceedings of the 1-st European Conference on Model-Driven Software Engineering, Nuremberg. ibmus AG, 2003, p. 55-63.
27. В.В.Кулямин, И.Б.Бурдонов, А.С.Косачев, Петренко А.К. Подход UniTesK к разработке тестов // Программирование, том 29, №6, 2003, стр. 25-43.
28. Е.Н.Бритвина, С.Г.Грошев, А.Монахов, А.К.Петренко, О.Л.Петренко. Тестирование на основе моделей // Открытые системы, Москва, № 9, 2003, стр. 41-47
29. С.В. Зеленов, С.А. Зеленова, А.С. Косачев, Петренко А.К. Генерация тестов для компиляторов и других текстовых процессоров // "Программирование", Москва, 2003, том. 29, N 3.
30. A.K.Petrenko. Specification Based Testing: Towards Practice. Perspectives of System Informatics // LNCS, No.2244, 2001, pp. 287-300.
31. Петренко А.К., Е.А.Кузьменкова Формальная спецификация программ на языке RSL (методическое пособие по практикуму). МГУ им. М.В.Ломоносова, Москва, 1999.
32. Ig. Burdonov, A. 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.
33. Петренко А.К. Технология программирования // Сборник "Современное состояние и тенденции развития информационных технологий в России", Миннауки, Научный совет по ГНТП "Информатизация России", 1995 г., стр.88-108.
34. I.Burdonov, A.KossatchevS.Cheng, H.Wong Formal Specification and Verification of SOS Kernel // BNR/NORTEL Design Forum, June 1996.
35. Петренко А.К. Методы отладки и мониторинга параллельных программ. Програмирование,3,1994.
36. Крюков В.А., Максимов А.В., Петренко А.К., Полилова Т.А. Иерархическое конфигурационное управление // Програмирование,2,1994.
37. Петренко А.К., Спецификация тестов на основе описания трасс // Программирование, 1, 1993.
38. Петренко А.К., Борисова М.В., Морозова Т.А., Чацкина Т.А Тестирование компиляторов на основе формальной модели языка // Препринт ИПМ, N 45, 1992.
39. Петренко А.К. Венский метод разработки программ - VDM. Неформальное введение // Программирование, N 6, 1990.
40. Петренко А.К. Проблемы построения базы данных для интегрированных сред // В кн.: IV Всесоюзная науч. конференция Системы баз данных и знаний НПО Центрпрограммсистем,Калинин, 1990.
41. Крюков В.А., Петренко А.К., Шура-Бура М.Р. Транслятор в системе автоматизации разработки // В сб.: Методы трансляции и конструирован. программ. Тез. Всес. конференции, Новосибирск, 1988.
42. Петренко А.К. Система Мимоза. Концепции и возможности. Препринт ИПМ АН СССР, N 4 1983.
43. Петренко А.К. Методы расширения интерактивных пакетов прикладных программ // В кн.:Разработка пакетов прикладных программ.Новосибирск, "Наука", 1982.
44. Петренко А.К. Разработка интерактивных пакетов программ в системе Мимоза // В сб.:Интерактивные системы Тез. докладов. Мецниереба, Тбилиси, 1981.
45. Петренко А.К. Интерактивная система общения с задачей - Мимоза // В сб.:Проблемы проектирования и применения дискретных систем в управл. Тезисы докл. Минск, 1977
46. Петренко А.К., Петренко О.Л. Машина Беббиджа и возникновение программирования // Истор.-математические исследования.- Вып. XXIV. М."Наука 1976.
47. Петренко А.К., Усов С.А. Диалоговый монитор - Димон. Запуск задач в пакет // Препринт ИПМ АН СССР,N 69 1975.

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

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

• А.Хорошилов 2006. Спецификация и тестирование компонентов с асинхронным интерфейсом.
• Н.Пакулин 2006. Формализация стандартов и тестовых наборов протоколов интернета.
• М.Архипова 2006. Автоматическая генерация тестов для семантических анализаторов трансляторов.
• А.Демаков 2006. Объектно-ориентированное описание графового представления программ и моделей.
• А.С.Камкин 2009. Метод автоматизации имитационного тестирования микропроцессоров с конвейерной архитектурой на основе формальных спецификаций.
• Д.Ю.Кичигин 2010. Метод редукции тестового набора для интеграционного тестирования.
• Д.В. Силаков 2010. Методы информационно-аналитической поддержки разработки и использования стандартов на интерфейсы операционной системы Linux.
• В.С. Мутилин 2012. Верификация драйверов операционной системы Linux при помощи предикатных абстракций.
• М.М.Чупилко 2012. Динамическая верификация цифровой аппаратуры на основе формальных спецификаций.
• E.M. Новиков 2013. Развитие метода контрактных спецификаций для верификации модулей ядра операционной системы Linux.

• Международный семинар по тестированию на основе моделей (Model Based Testing - MBT) 2004, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014 годы.
• Весенняя Spring Young Researchers Colloquium on Software Engineering, SyrcoSE 2007-2016.
• Конференции OS Day, 2014, 2015.