EAST-ADL2 is a domain-specific architecture descriptionlanguage to support the model-based developmentof automotive embedded systems. It emerged to manage thecomplexity of software and electronics in advanced automotiveapplications. The language focuses on the structural definitionfor functional specifications. Behavior is defined only on thecomponent level, in terms of functional blocks and their triggersand interfaces. The behavioral definition inside each functionalblock is not prescribed. This paper shows one approachto augment the language with precise syntax and semanticsfor behavior, and develops a procedure that transforms thecomposed behavioral model to the SPIN model for logicmodel checking. The contribution improves the modeling andverification capability of EAST-ADL2.