System-level design methodologies for embedded HW/SW systems face several challenges: In order to be susceptible to systematic formal analysis based on state-space exploration, a modelling notation with a simple formal semantics is desired. Architecture-level engineering practice demands notations which concentrate on certain aspects of system functionality, while other aspects (such as communication and scheduling) are implicitly encoded in the language semantics, and realized using HW/SW components such as operating systems and protocol stacks. We describe a system-level design methodology targeted for automotive control applications. Models in a simple graphical component-based input language are compiled into complex system models incorporating abstractions for hardware, operating systems, and inter-processor communication. System models are based on the synchronous AutoFocus notation and are used as a basis for formal analysis such as systematic worst-case response time analysis. The paper describes a reference architecture for implementation, the MoDe design notation, and the translation to system models along with an outlook giving a perspective for analysis.