• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • MicroTESK: An Extendable Framework for Test Program Generation
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
May 25, 2026
HSE Scientists Train Neural Network to 'Hear' Faults in Electric Motors
Researchers at the AI and Digital Science Institute of the HSE Faculty of Computer Science have developed a new method—the Signature-Guided Data Augmentation (SGDA) framework—that achieves 99% accuracy in motor fault detection and 86% accuracy in fault classification. The application of this approach can reduce industrial equipment repair costs, minimise downtime, and improve production safety. The study results have been published in Engineering Applications of Artificial Intelligence.
May 25, 2026
'The Humanities Serve as a Conscience'
Maria Mizernaia studies Soviet literature and the history of book publishing. In this interview for the HSE Young Scientists project, she discusses plans to publish a novel about besieged Leningrad, AI-provoked reflections on what it means to be human, and how novels can help satisfy our dopamine hunger.
May 25, 2026
Is It Possible to Predict a Citys Life Based on the Shape of Its Neighbourhoods?
Is it possible to predict, based on the configuration of streets and buildings, where a café will open or where traffic congestion will occur? Participants in the Spatial Analysis and Modelling of Urban Processes research and study group use open data and machine learning to identify universal patterns. Alexander Sheludkov and Eduard Somov discuss the purpose of comparing cities, the need for new forms of urban statistics, and how open data is transforming approaches to urban studies.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

MicroTESK: An Extendable Framework for Test Program Generation

P. 51–57 .
Tatarnikov A., Kamkin A., Сергеева Т. И., Утехин А. Б.

Creation of test programs and analysis of their
execution is the main approach to system-level verification of microprocessors. A lot of techniques have been proposed to automate test program generation, ranging from completely random to well directed ones. However, no “silver bullet” has been found. In good industrial practices, various methods are combined complementing each other. Unfortunately, there is no solution that could integrate all (or at least most) of the techniques in a single framework. Engineers are forced to use a number of tools, which leads to the following problems: (1) it is required to maintain duplicating data (each tool uses its own representation of the target design); (2) to be used together, tools need to be integrated (engineers have to deal with different formats and interfaces). This paper proposes a concept of an extendable framework (MicroTESK) that follows a unified methodology for defining test program generation techniques. The framework supports random and combinatorial generation and (what is even more important) can be easily extended with new techniques being implemented as the framework’s plugins.

Language: English
DOI
Text on another site
Keywords: formal specificationsформальные спецификациимикропроцессорыфункциональная верификациягенерация тестовых программextendibilityрасширяемостьfunctional verificationtest program generationmicroprocessors

In book

Proceedings of the 7th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2013
Proceedings of the 7th Spring/Summer Young Researchers’ Colloquium on Software Engineering, SYRCoSE 2013
Kazan: -, 2013.
Similar publications
Towards the Flexible Distribution Networks Design Using the Reliability Performance Metric
Shushpanov I., Suslov K., Ilyushin P. et al., Energies 2021 No. 14 Article 6193
At present, the entire world is moving towards digitalization, including in the electric power industry. Digitalization is in its heyday and a lot of articles and reports are devoted to this topic. At the same time, the least digitalized of the electrical networks are distribution networks that account for a very large share in electric ...
Added: December 29, 2021
Test Program Generator MicroTESK for RISC-V
Kamkin A., Чупилко М. М., Смолов С. А. et al., , in: 2018 19th International Workshop on Microprocessor and SOC Test and Verification (MTV).: Austin: IEEE Computer Society, 2018. P. 6–11.
The paper presents a test program generator for functional verification of RISC-V microprocessors. The generator is implemented on the base of MicroTESK framework and consists of formal specifications of RISC-V ISA and ISA-independent core. The specifications describe instructions' syntax and semantics and can be easily modified to support more instructions (including custom extensions). The core ...
Added: July 3, 2019
Введение в формальные методы верификации программ: учебное пособие
Kamkin A., М.: МАКС Пресс, 2018.
This textbook is devoted to formal methods for program verification and is based on the lectures given by the author at CMC MSU, DCAM MIPT, and FCS HSE. It describes the basics of such approaches as deductive analysis and model checking. The list of topics includes formal semantics of programming languages (operational and axiomatic semantics), ...
Added: November 2, 2018
Генератор тестовых программ для архитектуры RISC-V на основе инструмента MicroTESK
Tatarnikov A., Kamkin A., Проценко А. С. et al., Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) 2018 № 2 С. 2–8
In this paper, a specification-based test program generator for functional verification of RISC-V microprocessors is presented. The tool is based on the MicroTESK framework and consists of two main parts: (1) the formal specifications of the RISC-V ISA and (2) the ISA-independent generation core. Test programs are generated on the basis of the ISA specifications and test templates ...
Added: October 30, 2018
Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018
Yaroslavl: Ярославский государственный университет им. П.Г. Демидова, 2018.
Workshop on Program Semantics, Specification and Verification: Theory and Applications is the leading event in Russia in the field of applying of the formal methods to software analysis. Proceedings of the ninth workshop dedicated to formalisms for program semantics, formal models and verification, programming and specification languages, algebraic and logical aspects of programming. ...
Added: October 26, 2018
Specification-Based Test Program Generation for ARM VMSAv8-64 Memory Management Units
Kamkin A., Tatarnikov A., Смолов С. А. et al., , in: 2015 16th International Workshop on Microprocessor and SOC Test and Verification (MTV).: IEEE, 2015. P. 1–6.
In this paper, a tool for automatically generating test programs for ARM VMSAv8-64 memory management units is described. The solution is based on the MicroTESK framework being developed at ISP RAS. The tool consists of two parts: an architecture-independent test program generation core and VMSAv8-64 specifications. Such separation is not a new principle in the ...
Added: July 18, 2018
Maintaining ISA Specifications in MicroTESK Test Program Generator
Kamkin A., Tatarnikov A., Проценко А. С. et al., , in: 2017 18th International Workshop on Microprocessor and SOC Test and Verification (MTV).: IEEE, 2017. P. 10–14.
The specification-based approach is widely used for test program generation for functional verification of microprocessors. The size of microprocessor specifications is measured in thousands lines of code. Consequently, their maintenance requires significant effort. Typical maintenance activities include regular updates, substitution of deprecated functionality, and support for new revisions and implementation-defined features. Our team is working ...
Added: July 18, 2018
Управление данными: 25 лет прогнозов
С.Д. Кузнецов, Труды Института системного программирования РАН 2017 Т. 29 № 2 С. 117–160
In October 2013, the eighth meeting of researchers in the field of databases was held. The first such meeting took place in February 1988, so that 25 years passed between them. After each meeting, a report was published containing an overview of the current state of the field and a research program for the nearest ...
Added: February 12, 2018
Расширяемая среда генерации тестовых программ для микропроцессоров
Tatarnikov A., Kamkin A., Смолов С. А. et al., Программирование 2014 Т. 1 № 40 С. 3–14
Development of test programs and analysis of the results of their execution is the basic approach to verification of microprocessors at the system level. There is a variety of methods for the automation of test generation, starting with the generation of random code and ending with directed model-based test generation. However, there is no cure-all ...
Added: February 5, 2018
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit