The ever growing number of features that need to be included in embedded system designs to meet market requirements coupled with the continuous advances in implementation architectures make system level design increasingly difficult. Existing ad hoc design techniques are inadequate to yield designs that are correct-the-first-time and robust with respect to manufacturing process and environment variations. Raising abstraction level, reusing IPs, and exploiting correct-by-construction design methods have been effective at coping with design complexity. Yet, design optimization requires an overall methodology that takes into consideration the importance of the correct choice of implementation platforms for the efficient execution of the required functionality. The design space for the selection of implementation architectures is very large. Its efficient exploration is essential. To do so, functionality has to be clearly separated from architecture so that the association of functionality to a number of architectures can be done quickly without the need of having a complete implementation done. In addition, IP re-use requires attention for the communication structures to choose to integrate them. To evaluate the quality of an association of functionality to architecture, we need a way of computing the "cost" of this association. To do so, quantities such as timing, power and area have to be evaluated efficiently and accurately. Further, when organizing a particular functionality with concurrent behavior, or mapping it on an architecture that has resource limitation, the issue of execution coordination arises. Last but not least, an efficient methodology has to allow the use of different models and specifications for different parts of the design and has to deal with legacy parts of the design.

In this dissertation, I focus on some of the issues that the implementation of this methodology needs resolving: namely, how to deal with orthogonal concerns when an overall design has to be captured and analyzed, and how to manage the composition of heterogeneous parts expressed in different styles (imperative vs. declarative), abstraction levels and description languages.

The difficulty in dealing with "composition" when verifying a system either with simulation or formal methods is manifest. Each individual concern in the design description specifies only the aspect it is concerned with. It is necessary to find out how this aspect is related to other aspects in the overall design by looking at other parts of the description and their relations. An even harder task is to compose heterogeneous models, because these models stay in isolated semantics islands. To connect these islands, bridges must be built across different abstraction levels, different specification languages, and different styles of specifications.

In this dissertation, I address the problem of how to efficiently compose and validate orthogonal concerns and heterogeneous models. To handle orthogonal concerns, I devised static and dynamic analysis techniques to reduce run-time overhead in simulation, including an efficient simultaneous constraints handling technique, named event reduction, medium-centric constraint resolution, interleaving concurrent simulation, and quantity resolution speedup algorithms. To deal with heterogeneous models, I proposed a Buchi Automaton based technique to enforce Linear Temporal Logic (LTL) constraints; I also developed a regular expression-based communication semantics adaptation mechanism. As the backbone, I built a communication and co-simulation infrastructure to integrate models written in different languages and at different abstraction levels. These ideas were experimented and verified in the Metropolis design environment.