Verifying architectural models of embedded systems is desirable, since architecture can impact the performance and resource usageof the final system implementation. To fulfill this need, one could thinkof combining formal verification and testing to achieve proofs of systemcorrectness with respect to functional and extra-functional requirements.Our first step to accomplish this goal has concretized in the development of a framework that integrates architectural models described inEast-adl language with component-based model-checking techniques.The framework is supported by a tool called ViTAL, which captures thebehavior of East-adl functions as timed automata models, which canbe formally verified in the Uppaal Port model-checker that exploitsthe components-based semantics at the architectural level. Later, thesame formal models will help generate test-suites to provide support formodel-based testing.