Dr. Alexander K. Petrenko

Current positions:

Head of Software Engineering Department of
Institute for System Programming RAS

Chief Scientific Adviser of Linux Verification Center

Full Professor of System Programming Chair,
Computer Science Department of
Moscow State University (MSU)

ORCID: 0000-0001-7411-3831
ResearcherID: D-8658-2014
Scopus AuthorID: 8960673500
SPIN CODE: 2635-5573

Contact information:
Phone: +7(495)912-5317 ext. 404
Mobile: +7(916)156-3502
Fax: +7(495)912-1524
Address: A. Solzhenitsyna, 25
109004, Moscow, Russia
E-mail: petrenko < at > ispras < dot > ru
Skype: ak-petrenko7076
Biographical Sketch, CV
Research Interests
  • Software and hardware verification and validation
  • Model Based Testing
  • Formal Methods in Software Engineering
  • Formalization of IT standards, functional and safety requirements
  • Software Security
  • Software Engineering and Systems Engineering Tool Chains

Selected Publications
Journals:
    Journals:
  1. D. V. Efremov, V. V. Kopach, E. V. Kornykhin, V. V. Kulyamin, A. K. Petrenko, A. V. Khoroshilov, I. V. Shchepetkov. Runtime Verification of Operating Systems Based on Abstract Models.- Programming and Computer Software, 2023, 49(7), pp. 559–565.
  2. P. N. Devyanin, D. V. Efremov, V. V. Kulyamin V. V., Petrenko A. K., Khoroshilov A. V., Shchepetkov I. V. Modeling and verification of access control security policies in operating systems. - Hotline-Telecom, 2019, 216 p.
  3. P. N. Devyanin, V. V. Kulyamin, V. V., Petrenko, A. K., Khoroshilov, A. V., Shchepetkov, I. V. Comparison of methods for decomposing specifications on Event-B.- Programming, 42(4):17-26, 2016.
  4. V. V. Kulyamin, E. M. Lavrishcheva, V. S. Mutilin, A. K. Petrenko Verification and analysis of variable operating systems.- Proceedings of ISP RAS. Volume 28, Issue 3, 2016. Pp. 189-208.
  5. I. S. Zakharov, M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. K. Petrenko, A. V. Khoroshilov. Configurable system for static verification of operating system kernel modules. - Programming, No. 1, 2015, pp. 44-67.
  6. A. K. Petrenko, V. V. Kulyamin, A. V. Khoroshilov On the integration of formal methods in the problems of operating system verification. - Proceedings of ISP RAS. Volume 27, Issue 5, 2015. Pp. 175-190.
  7. E. A. Gerlits, V. V. Kulyamin, A. V. Maksimov, A. K. Petrenko, A. V. Khoroshilov, A. V. Tsyvarev. Operating system testing. - Proceedings of ISP RAS, Volume 26, 2014. Issue 1. Pp. 73-108.
  8. D. V. Buzdalov, S. V. Zelenov, E. V. Kornykhin, A. K. Petrenko, A. V. Strakh, A. A. Ugnenko, A. V. Khoroshilov. Instrumental means for designing integrated modular avionics systems. - Proceedings of ISP RAS, Volume 26, 2014, Issue 1, pp. 201-230.
  9. I. S. Zakharov, M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. K. Petrenko, A. V. Khoroshilov. “Configurable system for static verification of operating system kernel modules”. - Proceedings of ISP , Volume 26-2, 2014, pp. 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 Engineering and Formal Methods, Cape Town, South Africa, 10-14 November 2008.
  17. K. Petrenko, O. L. Petrenko, V. V. Rubanov. Creating an Open Educational Environment Based on Open Source Projects.- Abstracts of the Third Conference "Free Software in Higher Education", Pereslavl-Zalessky, February 2008, pp. 12-16.
  18. V. P. Ivannikov, A. S. Kamkin, A. S. Kosachev, V. V. Kulyamin, A. K. Petrenko. Using contract specifications to represent requirements for functional testing of hardware. - Programming, Vol. 33, No. 5, 2007, pp. 47-61.
  19. N. Pakulin, A. K. Petrenko, O. L. Petrenko, A. Sortov, A. Khoroshilov. Open standards and new forms of international cooperation. - Proceedings of ISP RAS, Vol. 13, Part 1, Moscow, 2007, pp. 7-30, ISBN 5-89823-026-2.
  20. V. P. Ivannikov, A. K. Petrenko. Verification tasks of Linux OS in the context of its use in the public sector.- Proceedings of ISP RAS, Vol. 10, Moscow, 2006, pp. 9-14, ISBN 5-89823-026-2/
  21. 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 9th 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. Kulyamin, I. B. Burdonov, A. S. Kosachev, A. K. Petrenko. The UniTesK approach to test development. - Programming, vol. 29, no. 6, 2003, pp. 25-43.
  25. E. N. Britvina, S. G. Groshev, A. Monakhov, A. K. Petrenko, O. L. Petrenko. Model-Based Testing. - Open Systems, Moscow, No. 9, 2003, pp. 41-47 26.
  26. S. V. Zelenov, S. A. Zelenova, A. S. Kosachev, A. K. Petrenko. Test generation for compilers and other text processors. - "Programming", Moscow, 2003, vol. 29, N 3 .
  27. A. K. Petrenko. Specification Based Testing: Towards Practice. Perspectives of System Informatics.-LNCS, No.2244, 2001, pp. 287-300.
  28. A. K. Petrenko, E. A. Kuzmenkova Formal specification of programs in the RSL language (methodological manual on practical training). Lomonosov Moscow State University, Moscow, 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. A. K. Petrenko. Programming technology. - Collection "Current state and development trends of information technologies in Russia", Ministry of Science, Scientific Council on State Scientific and Technical Program "Informatization of Russia", 1995, pp. 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. A. K. Petrenko. Methods of Debugging and Monitoring Parallel Programs. Programming, 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. V. A. Kryukov, A. V. Maksimov, A. K. Petrenko, T. A. Polilova. Hierarchical configuration management. - Programming, 2, 1994.
  35. A. K. Petrenko, Test specification based on trace description.- Programming, 1, 1993.
  36. A. K. Petrenko, M. V. Borisova, T. A. Morozova, T. A. Chatskina. Testing compilers based on a formal language model. - Preprint IPM, N 45, 1992.
  37. A. K. Petrenko. Vienna Method of Program Development - VDM. Informal Introduction. - Programming, N 6, 1990.
  38. A. K. Petrenko . Problems of constructing a database for integrated environments. - In the book: IV All-Union scientific conference Systems of databases and knowledge NPO Centerprogrammsystem, Kalinin, 1990.
  39. V. A. Kryukov, A. K. Petrenko, M. R. Shura- Bura. Translator in the development automation system. - In the collection: Methods of translation and design. programs. Abstracts. All-Union Conference, Novosibirsk, 1988.
  40. A. K. Petrenko. The Mimosa System. Concepts and Possibilities. Preprint IPM USSR Academy of Sciences, N 4 1983.
  41. A. K. Petrenko. Interactive system of communication with the task - Mimosa.- In the collection: Problems of designing and applying discrete systems in control. Abstracts of reports. Minsk, 1977
  42. A. K. Petrenko, O. L. Petrenko. Babbage Machine and the Origin of Programming. - Historical and Mathematical Research. - Issue XXIV. M. "Science" 1976.
  43. A. K. Petrenko, S. A. Usov. Dialogue Monitor - Dimon. Launching Tasks in a Batch. - Preprint IPM USSR Academy of Sciences, No. 69 1975.
Book Chapters & Conference Proceedings (Peer Reviewed):
  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. A.V. Khoroshilov, V.V. Kuliamin, A.K. Petrenko, O.L. Petrenko, V.V. Rubanov. Building Open Learning Environment for Software Engineering Students //B. O. Czerkawski, ed. Free and Open Source Software for E-Learning: Issues, Successes, and Challenges, pp.110-119, IGI Global, 2010.
  6. V.V. Kuliamin, V.A.Omeltchenko, O.L. Petrenko. Formal Methods: for All or for Chosen? //Proceedings of CSEDU 2009, v. 2, pp. 217-222, Lisboa, Portugal, March, 23-26, 2009.
  7. 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.
  8. 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
  9. S.V.Zelenov, D.V.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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. V. V. Kuliamin, A. K. Petrenko, N. V. Pakoulin, A. S. Kossatchev, and I. B. Bourdonov. Integration of Functional and Timed Testing of Real-time and Concurrent Systems //Proceedings of PSI'2003, Novosibirsk, Russia, July 9-12, 2003 LNCS 2890:450-461, Springer-Verlag, 2003.
  15. I. Bourdonov, A. Kossatchev, V. Kuliamin, and A. Petrenko. UniTesK Test Suite Architecture // Proceedings of FME'2002 (in FLoC'2002), Kopenhagen, Denmark, July 22-24, 2002, LNCS 2391:77-88, Springer-Verlag, 2002.
  16. A. Koptelov, V. Kuliamin, and A. Petrenko/ VDM++TesK: Testing of VDM++ Programs // Proceedings of the 3-rd VDM Workshop (in FloC'2002), Kopenhagen, Denmark, July 20-21, 2002, pp. 41-56.
  17. A.K.Petrenko. Specification Based Testing: Towards Practice. Perspectives of System Informatics // LNCS, No.2244, 2001, pp. 287-300.
  18. A.K.Petrenko, A.Vorobiev. Industrial Experience in Using Formal Methods for Software Development in Nortel Networks // Proceedings of Testing Computer Software Conference - TCS 2000, Washington, June, 2000.
  19. 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.
  20. A.K.Petrenko, M.V.Borisova, T.A.Morozova, T.A.Tchatskina. Compiler testing based on a language formal model // Preprint of KIAM, No. 45, 1992 (Russion).
  21. A.K.Petrenko, O.L.Petrenko. The Babbage machine and the origin of programming // Istor.-Mat. Issled., Moscow, “Nauka”, No. 24 (1979), 340-360 (Russian).

Refereed for:
  1. Programming and Computer Software,
  2. Journal of Systems and Software

Invited talks

Partners and Foundations:

Selected Projects
2021-present Development of the BOSRV real-time operating system
2017-present Development of the JetOS real-time operating system
2009-present System and Software Engineerong for Integrated Modular Avionics. Design and development of full life cycle support for integration testing of avionic software.
2008-present Linux Driver Verification (LDV). Static and dynamic techniques for driver verification of basicaly safety requirements.
2005-present Microprocessor designs testing. Enhancing of UniTESK for microprocessor unit and core test generation.
2006 - 2010 LSB (Linux Standard Base) Infrastructure Project. Information system and toolkit that addresses several interoperability issues for Linux distributions nad linux applications.
2005-2006 OLVER (Open Linux Verification Project). Formal specification of lbc and other root Linux libraries (about 1500 interfaces, including many POSIX functions) in fashion of pre- and post-condition of interface functions. UniTESK tool for test generation and test suites for 7 hardware platforms (part of official LSB certification test suite).
2000-2003 Intel’s Compiler Testing Project. Methodology and toolkit (OTK) for testing optimizing compilers. Provide effective, targeted mechanism for testing selected kinds of optimization.
1999 - present UniTESK Testing Technology. UniTESK enhances design-by-contract approach providing notations for contract specification in programming languages extensions and automatic test generation based on these specifications and test scenario specifications.
1994-1998 KVEST methodology and technology for test automation based on formal specification. KVEST used RSL (RAISE Specification Language) for API contract specification, test generation tool (RSL -> RSL) and translator RSL -> a proprietary programming language. KVEST was applied to Nortel real-time operating systems (DMS-100, XCore). API of OS kernel (about 600 interfaces) was formally specification and tested.
1989-1992 Compiler and formal specification of real-time programming language for “Buran” space shuttle. Methodology for systematic by-hand design of compiler test suites based on formal specification target language semantics presented as is-wf-functions.
1980-1983 Intelligent interactive shell for FORTRAN software. LISP extension by multithreading features to support rapid development of interactive wrappers for computational packages. Used in plasma diagnostics projects.
1977-1980 LISP compiler and interpreter. An experimental implementation of compiler based on macro-generation techniques. Interpreter. Bridge with FORTRAN libraries.
1975-77 Remote job control system DIMON.

Web resources

Supervised theses
  • A.Khoroshilov 2006. Specification and testing of components with asynchronous interfaces.
  • N.Pakulin 2006. Formalization of standards and test suites of internet protocols.
  • M.Arkhipova 2006. Automatic test generation for semantic analyzers of translators.
  • A.Demakov 2006. Object-oriented description of graph representations of programs and models.
  • A.S.Kamkin 2009. An automation method of simulation testing of pipeline microprocessor on the base of formal specifications.
  • D.Yu.Kichigin 2010. A method of test suite reduction for integration testing.
  • D.V.Silakov 2010. Information and analytical support methods for development and usage of standards on Linux operating system interfaces.
  • E.V.Kornykhin 2010. Testing programs generation for microprocessor memory management unites testing.
  • V.S. Mutilin 2012. Linux drivers verification using predicate abstractions.
  • M.M. Chupilko 2012. Dynamic verification of the digital equipment based on formal specifications.
  • E.M. Novikov 2013. Development of contract specifications method for verification of Linux kernel module.
Professional Activities

Organizer

Program Committee Chair
  • 1st-10th International Workshop on Model Based Testing – MBT at ETAPS federal conference
  • 1st-9th International Spring Young Researcher Colloquium on Software Engineering – SYRCoSE

Program Committee Member

Ph.D. Thesis Committees

Member of Editor-Board
  • Programming and Computer Software, in Russian and English
  • Proceedings of the Institute for System Programming of the RAS, in Russian and English
  • Software Engineering (Porgrammnaya inzheneria), in Russian

Member of Professional Organizations
  • IEEE Computer Society
  • ACM

Chair of Russian Subcommittee of Standardization Technical Committee22 / ISO/IEC JTC 1/SC 22 “Programming languages, their environments and system software interfaces”