Requirements modelling helps software engineers understand a system's required behaviour and explore alternative system designs. It also generates a formal software specification that can be used for testing, verification, and debugging. However, elaborating such models requires expertise and significant human effort. The paper aims at reducing this effort by automating an essential activity of requirements modelling which consists in deriving a machine specification satisfying a set of goals in a domain. It introduces deontic input-output automata - an extension of input-output automata with permissions and obligations - and an automated synthesis technique over this formalism to support such derivation. This technique helps modellers identifying early when a goal is not realizable in a domain and can guide the exploration of alternative models to make goals realizable. Synthesis techniques for input-output or interface automata are not adequate for requirements modelling.

Making decisions among a set of alternative system designs is an essential activity of requirements engineering. It involves evaluating how well each alternative satisfies the stakeholders' goals and selecting one alternative that achieves some optimal tradeoffs between possibly conflicting goals. Quantitative goal models support such activities by describing how alternative system designs - expressed as alternative goal refinements and responsibility assignments - impact on the levels of goal satisfaction specified in terms of measurable objective functions. Analyzing large numbers of alternative designs in such models is an expensive activity for which no dedicated tool support is currently available. This paper takes a first step towards providing such support by presenting automated techniques for (i) simulating quantitative goal models so as to estimate the levels of goal satisfaction contributed by alternative system designs and (ii) optimising the system design by applying a multi-objective optimisation algorithm to search through the design space. These techniques are presented and validated using a quantitative goal model for a well-known ambulance service system.