  Development of quality assured software-intensive systems, such as automotive
embedded systems, is an increasing challenge as the complexity of these systems
significantly increases. EAST-ADL is an architecture description language
developed to specify automotive embedded system architectures at multiple
abstraction levels in the development of safety-critical automotive products.
In this paper, we propose an architecture-based verification technique which
enhances the model-based development process supported by EAST-ADL by adapting
model-checking to EAST-ADL specifications. We employ UPPAAL as a verification
tool to ensure that predicted function behaviors of the models in EAST-ADL
satisfy functional and real-time requirements. The criteria for this
architecture-based verification is presented and the transformation rules which
comply with this criteria are derived. This enables us to extract the relevant
information from EAST-ADL specifications and to generate analyzable UPPAAL
models. The formal semantics of EAST-ADL is defined which is essential to
automate the verification of EAST-ADL specifications. Our approach is
demonstrated by verifying the safety of the steering truck system units.
