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:
  1. V.V. Kuliamin, E.M. Lavrischeva, V.S. Mutilin, A.K. Petrenko. Verification and analysis of variable operating systems Proceedings of the Institute for System Programming. Volume 28, issue 3, 2016 . pp. 189-208.
  2. I.S. Zakharov, M.U. Mandrykin, V.S. Mutilin, E.M. Novikov, A.K. Petrenko, A.V. Khoroshilov. Configurable toolset for static verification of operating systems kernel modules. Programming and Computer Software, January 2015, Volume 41, Issue 1, pp 49-64.
  3. Devyanin, P.N.,Khoroshilov, A.V.,Kuliamin, V.V.,Petrenko, A.K.,Shchepetkov, I.V. Using refinement in formal development of OS security model // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2016
  4. Zakharov, I.S.,Mandrykin, M.U.,Mutilin, V.S.,(...),Petrenko, A.K.,Khoroshilov, A.V. Configurable toolset for static verification of operating systems kernel modules, Programming and Computer Software, 2015.
  5. V.V. Kulyamin, A.K. Petrenko. Evolution of the UniTESK test development technology. Programming and Computer Software 40(5), 2014, pp. 296-304.
  6. 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.
  7. 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.
  8. V.P.Ivannikov, A.S.Kamkin, A.S.Kossatchev, V.V.Kuliamin, A.K.Petrenko. The use of contract specifications for representing requirements and for functional testing of hardware models // Programming and Computer Software, Vol.33, No. 5, 2007, pp. 272-282.
  9. V.V.Kuliamin, A.V.Khoroshilov, A.K.Petrenko, V.Rubanov. Interface standards formalization and automatic conformance tests generation // Information technologies No. 8, 2007, pp. 2-7, (Russian).
  10. V. V. Kuliamin, A. K. Petrenko, A. S. Kossatchev, and I. B. Burdonov. The UniTesK Approach to Designing Test Suites // Programming and Computer Software, Vol. 29, No. 6, 2003, pp. 25-43.
  11. S.V.Zelenov, S.A.Zelenova, A.S.Kossatchev, A.K.Petrenko. Test generation for compilers and other test processors// Programming and Computer Software, Moscow, 2003, Vol. 29, No. 3.
  12. E.N.Britvina, S.G.Groshev, A.A.Monakhov, A.K.Petrenko, O.L.Petrenko. Model Based Testing // Open systems, Moscow, No. 9, 2003, pp. 41-47.
  13. A.K.Petrenko. Parallel monitoring and debugging (survey). Programming and Computer Software, Vol. 20, No.,3,1994.
  14. V.A.Krukov, A.V.Maksimov, A.K.Petrenko, T.A.Polilova. Hierarchical configuration management // Programming and Computer Software, Vol. 20, No. 2, 1994.
  15. A.K.Petrenko. Test specification based on trace description // Programming and Computer Software, Vol. 19, No. 1, 1993.
  16. A.K.Petrenko. Vienna Development Method - VDM. Informal introduction // Programming and Computer Software, N 6, 1990.
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
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”