[khoroshilov.jpg]
Алексей Хорошилов, в.н.с. ИСП РАН
директор Центра верификации ОС Linux
Logo ISPRAS

Logo LinuxTesting

В 1986-1991 годах учился в средней школе №630 г. Москвы, в 1991-1995 годах — в физико-математическом классе при МФТИ в средней школе №503 г. Москвы, а в 1995-1996 годах — в Физико-математической школе №18 при МГУ, впоследствии переименованной в Специализированный учебно-научный центр МГУ. В 2001 году с отличием окончил факультет Вычислительной Математики и Кибернетики МГУ, в 2001-2004 г. обучался в аспирантуре факультета Вычислительной Математики и Кибернетики МГУ, на кафедре Системного программирования.

Кандидат физико-математических наук (2006 г.), тема диссертации - «Спецификация и тестирование компонентов с асинхронным интерфейсом», научный руководитель д.ф.-м.н. А.К. Петренко.

С 1999 года работает в Институте системного программирования РАН, на 2014 год — в должности ведущего научного сотрудника.

С 2009 года работает на кафедре Системного программирования факультета Вычислительной математики и кибернетики МГУ.

Основные научные интересы: методы проектирования и разработки ответственных систем, формальные методы программной инженерии, методы верификации и валидации, тестирование на основе моделей, методы анализа требований, операционная система Linux.

Автор и соавтор более 50 научных работ, в том числе:

  1. А.В.Хорошилов. “Спецификация и тестирование систем с асинхронным интерфейсом”. Препринт №12. М.: ИСП РАН, 2006.
  2. В. В. Кулямин, Н. В. Пакулин, О. Л. Петренко, А. А. Сортов, А. В. Хорошилов. Формализация требований на практике. Препринт. М.: ИСП РАН, 2006.
  3. В. В. Кулямин, А. К. Петренко, В. В. Рубанов, А. В. Хорошилов. Формализация интерфейсных стандартов и автоматическое построение тестов соответствия. // «Информационные технологии», 2007, №8, сс. 1-8.
  4. Н. В.Пакулин, А. В. Хорошилов. “Разработка формальных моделей и тестирование соответствия для систем с асинхронными интерфейсами и телекоммуникационных протоколов”. // Программирование, №6, 2007, сс. 26-55.
  5. A. Khoroshilov, V. Kuliamin, A. Petrenko, O. Petrenko, V. Rubanov. “Building open learning environment for software engineering students” in "Free and Open Source Software for E-Learning: Issues, Successes and Challenges" / Betul Ozkan Czerkawski, editor, ISBN 978-1-61520-917-0, pp. 110-119, Information Science Reference, New York, 2011.
  6. Alexey Khoroshilov, Igor Koverninskiy, Alexander Petrenko and Alexender Ugnenko. "Integrating AADL-based Tool Chain into Existing Industrial Processes". // In Proceedings of 16th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS-2011), pp. 367-371, ISBN: 978-1-61284-853-2, Las Vegas, USA, April 27-29, 2011.
  7. Д. В.Силаков, А. В. Хорошилов. “Методы обеспечения переносимости ПО”. // Программирование, Том 37, 2011, №1 сс. 57-66.
  8. Мутилин В.С., Новиков Е.М., Страх А.В., Хорошилов А.В., Швед П.Е. “Архитектура LINUX DRIVER VERIFICATION”. Труды Института Системного Прогаммирования, Том 20, 2011, с. 163-187.
  9. Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A., Towards an Open Framework for C Verification Tools Benchmarking. // In Proceedings of the Eighth International Andrei Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS» (PSI 2011), 82-91, Novosibirsk, Russia, June 27 - July 1, 2011.
  10. Y. Gerlits, A. Khoroshilov. "Model-Based Testing of Safety Critical Real-Time Control Logic Software" // In Proceedings of the Seventh Workshop on Model-Based Testing (MBT 2012), Tallin, Estonia, March 25, 2012.
  11. M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. V. Khoroshilov, and P. E. Shved "Using Linux Device Drivers for Static Verification Tools Benchmarking" //Programming and Computer Software, 2012, Volume 38, Number 5, Pages 245-256. DOI: 10.1134/S0361768812050039
  12. Мутилин В.С., Новиков Е.М., Хорошилов А.В. “Анализ типовых ошибок в драйверах операционной системы Linux”. Труды Института Системного Программирования, Том 22, 2012, с. 349-374.
  13. 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.
  14. Новиков Е.М., Хорошилов А.В. “Использование аспектно-ориентированного программирования для выполнения запросов по исходному коду программ”. Труды Института Системного Программирования, Том 23, 2012, с. 371-386.
  15. М.У. Мандрыкин, В.С. Мутилин, А.В. Хорошилов. “Введение в метод CEGAR — уточнение абстракции по контрпримерам”. Труды Института Системного Программирования, Том 24, 2013, с. 219-292.
  16. Е.А. Герлиц, В.В. Кулямин, А.В. Максимов, А.К. Петренко, А.В. Хорошилов, А.В. Цыварев. “Тестирование операционных систем”. Труды Института Системного Программирования, Том 26-1, 2014, с. 73-108.
  17. Д.В. Буздалов, С.В. Зеленов, Е.В. Корныхин, А.К. Петренко, А.В. Страх, А.А. Угненко, А.В. Хорошилов. “Инструментальные средства проектирования систем интегрированной модульной авионики”. Труды Института Системного Программирования, Том 26-1, 2014, с. 201-230.
  18. 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
  19. И.С. Захаров, М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.К. Петренко, А.В. Хорошилов. “Конфигурируемая система статической верификации модулей ядра операционных систем”. Труды Института Системного Программирования, Том 26-2, 2014, с. 5-42.
  20. D.Buzdalov, A.Khoroshilov. "A discrete-event simulator for early validation of avionics systems". Proceedings of the First International Workshop on Architecture Centric Virtual Integration - ACVI 2014, Valencia, Spain, September 29, 2014. CEUR‑WS Vol-1233, pp.28-38.
  21. Павел Андрианов, Алексей Хорошилов, Вадим Мутилин "Lightweight Static Analysis for Data Race Detection in Operating System Kernel". Материалы международной научно-практической конференции Инструменты и Методы Анализа Программ (TMPA-2014), с.128-135, 14-15 ноября 2014, Кострома, Россия.
  22. П.Н. Девянин, В.В. Кулямин, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков "О представлении МРОСЛ ДП-модели в формализованной нотации Event-B". «Проблемы информационной безопасности. Компьютерные системы», №3, 2014, сс.7-15.
  23. Д.В. Буздалов, Е.В. Корныхин, А.А. Панфёров, А.К. Петренко, А.В. Хорошилов "Практикум по дедуктивной верификации программ" (учебно-методическое пособие), "МАКС-Пресс", Москва, 2014. ISBN: 978-5-317-04884-6
  24. A. V. Khoroshilov, M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. K. Petrenko, and I. S. Zakharov "Configurable toolset for static verification of operating systems kernel modules" //Programming and Computer Software, 2015, Volume 41, Number 1, Pages 49-64.
  25. A. V. Khoroshilov, V. S. Mutilin, I. S. Zakharov "Pattern-based environment modeling for static verification of Linux kernel modules" //Programming and Computer Software, 2015, Volume 41, Number 3, Pages 183-195.
  26. M. U. Mandrykin, A. V. Khoroshilov "High-Level Memory Model with Low-Level Pointer Cast Support for Jessie Intermediate Language" //Programming and Computer Software, 2015, Volume 41, Number 4, Pages 197-207.
  27. Petr N. Devyanin, Alexey V. Khoroshilov, Victor V. Kuliamin, Alexander K. Petrenko, Ilya V. Shchepetkov "Using Refinement in Formal Development of OS Security Model". In Lecture Notes in Computer Sciences #9609 "Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference", pp. 107-115, Springer International Publishing.
  28. Д.В. Ефремов, Н.Ю. Комаров, А.В. Хорошилов. "Конструирование ядра операционной системы", Издательский отдел факультета ВМК МГУ имени М.В. Ломоносова, Москва, 2015. ISBN: 978-5-89407-549-5
  29. П.С. Андрианов, В.С. Мутилин, А.В. Хорошилов. “Метод легковесного статического анализа для поиска состояний гонок”. Труды Института Системного Программирования РАН, Том 27-5, 2015, с. 87-116.
  30. А.В. Цыварев, А.В. Хорошилов. “Использование симуляции сбоев при тестировании компонентов ядра ОС Linux”. Труды Института Системного Программирования РАН, Том 27-5, 2015, с. 157-174.
  31. M.U. Mandrykin, A.V. Khoroshilov "Region analysis for deductive verification of C programs" //Programming and Computer Software, 2016, Volume 42, Number 5, Pages 257-278.
  32. Pavel Andrianov, Vadim Mutilin, Alexey Khoroshilov "Predicate abstraction based configurable method for data race detection in Linux kernel". // In Communications in Computer and Information Science #779 "TMPA 2017: Tools and Methods of Program Analysis", pp. 11-23.
  33. Хорошилов А.В., Щепетков И.В. ADV_SPM — Формальные модели политики безопасности на практике // Труды Института системного программирования РАН. — 2017. — Т.29, №3. — С. 43–56.
  34. Mikhail Mandrykin, Alexey Khoroshilov "A Memory Model for Deductively Verifying Linux Kernel Modules". In Lecture Notes in Computer Sciences #10742 "Perspectives of System Informatics: 11th International Andrei P. Ershov Informatics Conference", pp. 256-275.
  35. Denis Efremov, Mikhail Mandrykin, Alexey Khoroshilov. Deductive Verification of Unmodified Linux Kernel Library Functions. 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part II. 216-234. 10.1007/978-3-030-03421-4_15.
  36. Cheptsov V., Alexey Khoroshilov A. Dynamic Analysis of ARINC 653 RTOS with LLVM // IEEE The Proceedings of the 2018 Ivannikov ISPRAS Open Conference (ISPRAS-2018) 2018. P. 9-15.
  37. Кильдишев Д.С., Хорошилов А.В. Формализация метамодели системы управления требованиями. Труды ИСП РАН, том 30, вып. 5, 2018 г., стр. 163-176 (на английском языке).
  38. П.Н. Девянин, Д.В. Ефремов, В.В. Кулямин, А.К. Петренко, А.В. Хорошилов, И.В. Щепетков. Моделирование и верификация политик безопасности управления доступом в операционных системах. Горячая линия – Телеком Москва, 2019.

См. также список публикаций на Google Scholar.

Координаты

Комната: 202
Телефон: +7 (495) 912-53-17(доб. 428)
GPG-Key: 0x30B0AC45,
Контрольная сумма: 063C 7488 A55F E669 0A3D A647 D81F C94B 30B0 AC45
Почтовый адрес:
Институт системного программирования им. В.П. Иванникова Российской академии наук
109004 Россия, Москва, А. Солженицына, 25.