Formal incremental requirements specification of service-oriented automotive software systems

In this paper, we introduce a simple but formal service description language (ForSeL) for modelbased requirements engineering. The basic notion in ForSeL is a service representing a functional requirement. Each service describes a system "re"-action that is triggered by a set of input actions -- (but only) if an additional precondition holds. The functional part of a specification is then obtained by the combination of a finite number of services. We pay special attention to two kinds of preconditions which are often mixed up in practice: sufficient and necessary preconditions. Moreover, we present refinement concepts for services that enable a stepwise development of functional requirements.