Test case generation and specification validation are essential concerns for the software industry in its continuous search for productivity improvement and quality mastering. This paper presents the approach developed in the MUTATION project for functional test case synthesis in the THALES industrial context. A two-step approach is proposed, which automates most of the process in a continuous way. The first step consists in expressing the requirements in the Requirements Description Language (RDL) textual formalism and completing, disambiguating and validating them through simulation. Test objectives are then automatically derived from the RDL formalisation. The second step synthesises functional test cases through combining the test objectives produced at step 1 and symbolic path computation on a UML detailed design model of the application, using the academic tool AGATHA (French acronym for toolset dedicated to automatic test generation for automata based specification). Test cases are produced through selecting symbolic behaviour paths that match the test objectives, applying a constraint solver to generate numeric tests. This approach is based on three innovations that are the core of this work: 1) definition of an appropriate language and a related methodology to define the test requirements; 2) symbolic execution on a UML action language; 3) combination of test objectives and symbolic execution to synthesize functional test cases.