Formal methods have come into use for the construction of real systems, as they help increase software quality and reliability. However, they are usually accessible only to specialists, thus discouraging stakeholders' participation, crucial in first steps of software development. To address this problem, we present in this paper a strategy to derive an initial formal specification, written in the RAISE Specification Language, from requirements models based on natural language, such as the Language Extended Lexicon, the Scenario Model, and the Business Rules Model, which are closer to the stakeholders' language. We provide a set of heuristics which show how to derive types and functions, and how to structure them in a layered architecture, thus contributing to fruitfully use the large amount of information usually available after requirements modelling stage. In addition, we illustrate the strategy with a concrete case study.