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.