Core Technologies
The Unit Verification and Core Technologies (UVCT) group is responsible for the development of the core technologies.
Background to Model Based Test Generation
Model-Based Test Generation (MBTG), an approach to test generation that has been championed by IBM, is based on the separation of the domain-specific model from a domain-independent generation engine. This separation of model from engine yields two advantages:
- The complexity of the overall system (and in particular, the test generation engine) is reduced by the modularization of concerns.
- The problem domain is made more comprehensible and extensible by being described in a formal declarative model.
Over the past decade, IBM R&D Labs in Israel has developed a number of tools that have adopted the MBTG approach, including GPro for processor verification, Piparazzi for pipeline verification, X-Gen for system verification, and DeepTrans for address translation verification.
The two main core technologies
- The Generation Core (GEC) technology
The GEC technology is a powerful and generic toolbox for the development of model-based random test generators. It captures the essence of a model-based stimuli generation framework and provides powerful, universal constraint-solving mechanisms under a generalized object-oriented modeling scheme. This technology promotes a driver-slave approach, where the development of new applications can focus on the specifics of the targeted area, rather than on the recurring and often fastidious basics of test generation. This yields faster development with higher quality, as new applications readily benefit from the rich accumulated experience incorporated in their core.
- ClassMate - the modelling technology
A critical component of these model-based test generators is the ability to model the underlying problem domain. For a processor verification tool such as GPro, a typical architecture may include hundreds of instructions, dozens of resources (e.g., memory, registers), and a number of complex functional units (e.g., floating point, external interrupt mechanism). All this architectural information must be defined formally in the system's declarative model.
Test generation technology eventually evolved into a framework where the generation task is translated into a constraint satisfaction problem (CSP) and the generation process is based on constraint solving. This framework forms the backbone of the above mentioned test generators. Therefore, in addition to the structural information and testing knowledge of the domain, the modeling of constraints forms an integral part of the domain problem description.
ClassMate is an environment used for defining the complex domain models that underlie all of Haifa's model-based test generators. It consists of:- An expressive modeling language for defining complex types and constraints between types for defining the CSP problem
- A graphical user interface for facilitating the writing of the model
- An API for accessing the type and constraint information defined
Manager
Laurent Fournier,
