Scenario-based specifications have gained wide acceptance in requirements engineering. However, scenarios are not appropriate to describe global, system-wide invariants. Thus, a specification often consists of scenarios and universal properties. In order to obtain a consistent specification, the scenarios must be integrated in a way which does not violate the properties. However, manual integration of scenarios is an error-prone and laborious process. In the presented paper we suggest a synthesis algorithm for automatic integration of system scenarios to an overall specification with guaranteed satisfaction of system-wide safety properties. The main idea is to compute inter-scenario priorities, which disable certain scenarios if they violate a property.

This paper introduces an extractive approach to building-up a product line based on existing systems. Thereby, we focus on the analysis of common functionalities across different systems. Our commonality analysis is performed on the functional level which offers the highest reuse potential. We use the service diagram, a formally founded specification technique, for the functional specification. This allows us to perform the commonality analysis based on a formal definition of the system behavior. Concepts for the comparison of service diagrams and a methodology for building-up a service diagram of a product line are described in the paper. Additionally, since legacy systems rarely have an accurate functional specification, we present a methodology for extracting such a specification out of a given logical architecture.

Abstract Formal verification of software systems is a challenge that is particularly important in the area of safety-critical automotive systems. Here, approaches like direct code verification are far too complicated, unless the verification is restricted to small textbook examples. Furthermore, the verification of application logic is of limited use in industrial context, unless the underlying operating system and the hardware are verified, too. This paper introduces a generic model stack, allowing the verification of all system layers as well as the concrete application models being used in the upper layers. The presented models and proofs close the gap between the correctness proof for the lower layers of car electronics developed at the Saarland University and the verification procedure for distributed applications developed at the Technische Universität München.

Increasing complexity due to the multitude of different functions and their interactions as well as a rising number of different product variants are just some of the challenges that must be faced during the development of multi-functional system families. Addressing this trend we present an approach combining model-based development with product line techniques aiming at a consistent description of a software product family as well as supporting the configuration of its variants. We integrate the concept of variability in our framework [7] which only supported the representation of single software systems on subsequent abstraction levels so far. For the configuration of a concrete product we extend this framework by a feature-based model which allows to configure and derive single systems from a system family model. Furthermore, we explain how the complexity due to the possibly huge amount of configuration decisions can be handled by means of a staged configuration process.