tems. STARS manipulates abstract representations of system components to obtain upper bounds on the number of various events in the system, as well as a bound on the response time. VCC is a commercial discrete event simulator, that can be used both for functional and performance verification. We describe an extension of VCC to facilitate STARS. The extension allows the user to specract representations of VCC modules. These abstractions are used by STARS, but their validity can also be checked by VCC simulation. We also propose a mostly automatic procedure to genese abstractions. Finally, we illustrate on an example how STARS can be combined with simulation to find bugs that would be hard to find by simulation alone. ¨© ¤ ¥ § ¤ STARS (STatic Analysis of Reactive Systems) is a methodology for worst-case analysis of embedded systems [2, 3]. It can be used to verify different properties of systems, such as power consumption, timing performance, or resource utilizatio...