We propose a novel approach to tackle the design-productivity gap existing in the field of complex and heterogeneous embedded computing systems. We take as a starting point the SystemJ programming language, which combines the data processing and encapsulation elegance of Java with with the reactivity and synchrony of Esterel and the asynchronous decoupling of CSP (that is, with rendezvous communications). Our research proposal aims at improving SystemJ in two directions: first for the formal verification of SystemJ programs, and second for the automatic synthesis of hardware/software embedded code. An implementation within a complete tool is also planned. These two goals will help SystemJ becoming one of the leading system-level design language for complex and heterogeneous embedded systems. The first goal (formal verification) is essential for the validation of the system under design. As embedded computing systems are often safety-critical, formal verification is a crucial feature for a system-level design tool. We shall use observer-based model-checking, with state-space reduction techniques. The second goal (code synthesis) is crucial too because it avoids the tedious and error-prone phase of manual coding from the high-level specification. Instead, we shall be able to generate automatically a mixed hardware and software implementation, proven to be faithful to the high-level specification written in SystemJ. Such a proof of faithfulness shall be based on the formal semantics of SystemJ. These scientific research results shall be implemented within a tool suite, and we shall conduct case studies to evaluate its practical usefulness for the design of embedded systems as well as its performances.