The article presents a component-based approach to construction of a model based testing framework. The main idea underlying the approach is non-invasive composition, which allows integration of a set of components along with their further reconfiguration without changing their code, and so with minimal effort. The article outlines the architecture of a model based testing framework using this idea and describes a prototype of such a framework implemented on the base of free libraries and tools. Test development case study in the prototype framework is also presented.

This article describes an architecture of extensible modular system for logging and analysis of log files with complex structure. This system supports log format extension, isolation and selection of data and linking of heterogeneous data. Different methods of heterogeneous data linking are considered, including linking by content and by time marks. Also report generation is reviewed and an architecture of report generator that allows make reports from independent different modules is described.

The article is devoted to core-level functional verification of memory management units. The article presents method of directed test cases generation. This generation supposes systematic construction of test programs by given test templates. The proposing method has been applied to test cases generation for memory management units of MIPS64-compatible microprocessors.

This paper describes language for processor instructions specification created by the authors and application of this language for developing plug-ins for architecture support for TrEx. There is also included an analysis of pros and cons of this approach for plug-ins development.

In this work, a method for the automated test programs generation aimed at the verification of microprocessor control logic is considered. The method is based on formal specification of a microprocessor instruction set and description of pipeline hazards templates. The use of formal specifications allows automating development of test program generators and systematically testing control logic. At the same time, since the approach utilizes high-level descriptions that do not take into account cycle-accurate functioning of a pipeline, all the specifications and templates developed, as well as the constructed test programs, can be reused when the microarchitecture is modified. It makes it possible to apply the method at early stages of the microprocessor design cycle when frequent design changes are possible.

This paper touches upon the problem of the system testing of interconnected hardware modules when the resulted hardware design cannot be verified by means of module-level techniques due to its complexity. Brief analysis of the ways to develop test systems based on formal specifications is made in the paper. Also the method of verification is suggested which extends the module-based approach implementing the UniTESK technology.

In this work, some issues of automated construction of test programs intended for functional verification of branch units of microprocessors are considered. Problems appearing when creating such programs are defined, and techniques for their automated solution are suggested. The article focuses on the general issues of branch processing mechanisms and does not touch upon the problems specific for concrete microprocessor architectures. The suggested techniques can be used in industrial test program generators.

The paper presents conformance test suite for new Internet Protocol Security Suite IPsec v2. The test suite was constructed by means of the UniTESK automated testing technology and its implementation, CTESK toolkit.
The work was done in the Institute for System Programming of RAS within “Verification of security functions of the next generation protocol IPsec v2” supported by RFBR grant 07-07-00243. The project included elicitation of requirements for implementations, development of formal specification and prototype test suite for IPsec v2 including the protocol of key exchange IKE v2. The paper discusses the method of formalization of IPsec v2 requirements, test suite development process, and results of test suite application to the existing implementations. The application shows that the method presented in the paper allows for construction for efficient testing automation for such complex protocols like security protocols.

The paper is concerned with conformance testing, which checks conformance relation between behavior of some software or hardware system and its requirements specification. Safe testing approach suggested by authors for refusal trace-based conformance is applied to weak simulation conformance, which uses some relation between states of specification and implementation models. The article presents the theory of safe simulation conformance and its testing. We suggest a general algorithm of complete testing and its more practical modification applicable to restricted classes of specifications and implementations.

One of the approaches to provide application security in the context of untrusted operating system is to use dedicated virtual machine to service certain hardware devices that may be used to compromise data (e.g. network adapter may be used to leak sensitive data). In such architecture it is necessary to somehow provide access to the hardware in the other virtual machine for the trusted applications bypassing the original operating system mechanisms. This article describes a solution for such problem based on the remote system call execution. The presented approach uses hardware virtualization and allows executing system calls remotely without modifying neither application nor operating system code.

В статье описывается разработанная в ИСП РАН система моделирования распределенных вычислительных сред Grid. С помощью этой системы проведен анализ реальной вычислительной среды Sharcnet. На основе анализа были выявлены возможные способы существенного увеличения эффективности работы среды.