The work presented in this thesis deals with modeling, specification and testing of models of Systems-on-a-Chip (SoCs) at the transaction abstraction level and higher. SoCs are heterogeneous: they comprise both hardware components and processors to execute embedded software, which closely interacts with hardware. SystemC-based Transaction Level Modeling (TLM) has been very successful in providing high-level executable component-based models for SoCs, also called virtual prototypes (VPs). These models can be used early in the design flow for the development of the software and the validation of the actual hardware. For SystemC/TLMvirtual prototypes, Assertion-Based Verification (ABV) allows property checking early in the design cycle,helping to find bugs early in the model and to save time and effort that are needed for their fixing. TL model scan be over-constrained, which means that they do not represent all the behaviors of the hardware, and thus,do not allow detection of some malfunctions of the prototype. Our contributions consist of two orthogonal and complementary parts: On the one hand, we identify sources of over-constraints in TL models appearing due to the order of interactions between components, and propose a notion of loose-ordering which allows to remove these over-constraints. On the other hand, we propose a generalized stubbing mechanism which allows the very early simulation with SystemC/TLM virtual prototypes.We propose a set of patterns to capture loose-ordering properties, and define a direct translation of these patterns into SystemC monitors. Our generalized stubbing mechanism enables the early simulation with SystemC/TLM virtual prototypes, in which some components are not entirely determined on the values of the exchanged data, the order of the interactions and/or the timing. Those components have very abstract specifications only, in the form of constraints between inputs and outputs. We show that essential synchronization problems between components can be captured using our simulation with stubs. The mechanism is generic;we focus only on key concepts, principles and rules which make the stubbing mechanism implementable and applicable for real, industrial case studies. Any specification language satisfying our requirements (e.g., loose-orderings) can be used to specify the components, i.e., it can be plugged in the stubbing framework. We provide a proof of concept to demonstrate the interest of using the simulation with stubs for very early detection and localization of synchronization bugs of the design.