Customers of products that include or are determined by software today expect the product to be individually configurable. At the same time high quality and short delivery times are expected. As a consequence, the producer of the software must be able to develop systems that can be easily configured according to the customer's needs in such a way that each individually configured system satisfies all quality requirements. Especially in the case of high numbers of possible configurations, it is obvious that it is not feasible to construct all system configurations and check the properties of each of them. Rather, there must be means to assure quality generically, meaning once and for all configurations at the same time. This chapter considers software product line engineering as the base technology for how to construct configurable systems and add generic quality assurance means to this process. The mechanism can be understood as a general pattern explaining how to carry over quality assurance techniques to configurable systems. This is done for two concrete techniques in the chapter: model-based testing as a technique for the assurance of functional quality and model-based deployment as a technique for the assurance of real-time properties such as responsiveness, availability, and reliability. The techniques are demonstrated using the example of a configurable flight management system as found in modern airplanes.

In a model based software development process different kinds of modelling techniques are used for the specification of different aspects of systems. Thereby mostly visual techniques like UML diagrams are used, due to their comprehensibility, clarity, and wide acceptance. In order to obtain a consistent complete specification of the whole system the different models have to be integrated, i.e., conceptually they have to be considered as one specification. For that purpose comparisons, consistency checks, and integrations for models or specifications of different kinds of techniques are needed. In this paper a formal semantic approach to the integration of UML diagrams and other (visual) specification techniques is discussed that is based on a reference model as common semantic domain for all specifications.

The formal specification of multiple viewpoints of a system requires multiple specification formalisms, suitable for the specific concerns of the viewpoints. For rather different viewpoints, such as for instance the information and the computational model of a component of a system, even the underlying paradigms of the specification formalisms may be different. In this paper a general semantical framework for the formal specification of dynamically evolving systems is presented. Its models, algebra transformation systems, have states whose internal data structures are given by partial algebas, which are manipulated by the application of replacement rules. Its paradigm is the descriptive one of general model theory respectively institutions. Partial observations of the internal state structures yield a translation from algebra transformation systems to labelled transition systems, the granularity of which is determined by the specification of the admissible observations. Since labelled transition systems can be considered as the general (operational) models for process calculi, this translation allows comparisons between the descriptive paradigm of the model theoretic approach and the operational one of process calculi. Thus consistency checks of multiple viewpoint specifications are supported.

In order to model some features of object-oriented programming and system design algebraic and projection specifications (= process specifications) are combined in such a way, that declaration and manipulation of objects become basic features of specification. As class definitions algebraic module specifications with import and export interface, parameter and body part are used, with module interconnection mechanisms like union and extension to simulate strict inheritance.

The importance of a precise definition of what constitutes a software component and how to describe it have become critical issues in the considerations about enhancements of the software development process in general and reuse of software pieces in particular (see e.g. [Boo 87]). We consider these issues by first determining some requirements for component description languages. Based on that we discuss the Π-language as a candidate for a component description language. The Π-language was developed primarily for the specification of distributed modular systems, where the notions of data abstraction and concurrency play an equally important role. After describing the underlying concepts and the syntax of the Π-language we outline an attempt to define its formal semantics by means of algebraic module specifications.

The concept of projection specifications was recently introduced as a purely algebraic approach to the specification of continuous algebras in the framework of metric spaces. It allows to combine data type- and process specifications within one formalism. Parameterized projection specifications, corresponding to usual algebraic parameterized specifications, carry over compositionality to combined data type and process specifications. The parameter part may contain data types as well as process types. Transformation concepts for algebraic specifications are shown to apply also to projection specifications; i.e. extension and refinement, and different notions of implementation can be generalized to projection specifications.

The algebraic approach to the semantics of (nonterminating) processes based on the metric completion of process algebras is extended in two directions. Instead of adopting the predefined metric, it is proposed to define the metric internally, using a suitable family of projections as part of the specification and deal with projection spaces rather than metric spaces. It is also proposed to define the data type along with the processes, to allow nonconstant actions and internally defined communication functions. Combined data type and process specifications find a suitable basis for their algebraic semantics in projection algebras.

Integration is a necessary activity in each software development process. Within a model-based approach also the models that are used must be integrated. Model integration has two dimensions: On the one hand, the model components that result from the decomposition of the system under consideration have to be put together. On the other hand, different views onto the system are distinguished and modelled separately in order to decrease the complexity of the development process; the according models also must be brought together again. Integration models are meta-level definitions of model integration methods. Ideally they can be instantiated with arbitrary kinds of models and modelling languages, which then yields an integration method for these models. In this introduction integration modelling is put into perspective; integration models are presented in the following contributions.

Integration is a necessary activity in each software development process. Within a model-based approach also the models that are used must be integrated. Model integration has two dimensions: On the one hand, the model components that result from the decomposition of the system under consideration have to be put together. On the other hand, different views onto the system are distinguished and modelled separately in order to decrease the complexity of the development process; the according models also must be brought together again.Integration models are meta-level definitions of model integration methods. Ideally they can be instantiated with arbitrary kinds of models and modelling languages, which then yields an integration method for these models. In this introduction integration modelling is put into perspective; integration models are presented in the following contributions.

Due to the special requirements of distributed systems, it is important that modeling techniques for this kind of systems offer a stringent module concept. Each module has to support the encapsulation of data structure as well as functionality also at runtime. Modular graph transformation, presented in this contribution, supports these features. Modules are built up of specifications where attributed graphs describe the static data structures, whereas the dynamic behavior is modeled by the controlled application of graph rules. Rule expressions are used to formulate the control flow. Within one module, we can state a (weak) preservation of export and import behavior wrt. the local behavior in the module’s body in the sense that an interface derivation is subsumed by a local derivation if it can be performed. Modules may use each other meaning that each import interface has to be connected with an export interface in a way that the import behavior is subsumed by the export behavior.

Graph transformation systems are a formal specification technique for software systems that support the rule based specification of the dynamic behaviour of a system.Their main advantages are the intuitive visual representation of states and state transformations as graphs on the one hand, and the fully formal semantics on the other hand, that allow precise statements about the specification and tool support. In this paper we introduce refinements and modules for typed graph transformation systems to support the software specification development in both dimensions: modules for the horizontal structuring of a specification, i.e., its composition from feasible parts, and refinements for the development over time.

In a model-based software systems development formal specifications of the components of the system are developed. Thereby different specifications are used to represent the different aspects or views of the components, possibly following different paradigms. These heterogeneous viewpoint specifications have to be integrated in order to obtain a consistent global specification of the whole system. In this paper transformation systems are introduced as a common semantic domain where specifications written in different languages can be interpreted and formally compared. A transformation system is a transition system where the transitions are labelled by sets of actions and the states are labelled by algebras representing the data states. Development relations and composition operations for transformation systems are investigated, and it is shown that compatible local developments of components induce a global development of their composition. As an application two specifications of the alternating bit protocol are formally compared component-wise, one given in the process calculus CCS, the other one in the parallel programming language UNITY.

There is a variety of different approaches to the specification of software systems based on graph rewriting. In order to relate these and other state and/or rules based approaches algebra transformation systems have been introduced. They constitute a semantic domain that is independent of the way in which the rewriting of graphs or algebras is defined (implemented). Composition operations and refinement relations have been defined for algebra transformation systems that yield a comprehensive semantic specification framework in this way. Corresponding notions of rewriting, transformation system, composition and refinement in the different graph rewriting approaches can be compared with these semantic notions to relate them and exhibit their compatibility.

Wenn wir mathematische Sätze formulieren, dann machen wir nicht nur Aussagen, sondern wir geben auch an, unter welchen Voraussetzungen diese Aussagen gelten. Und wenn wir aus bewiesenen Sätzen neue Satze beweisen, dann ziehen wir nicht nur Folgerungen aus den darin gemachten Aussagen, sondern wir verbinden auch die Voraussetzungen dieser Aussagen zu den Voraussetzungen des neuen Satzes. Sequenzenkalküle bilden diese Vorgehensweise formal nacho Wir geben in diesem Kapitel einen Sequenzenkalkül für die Aussagenlogik an und beweisen seine Korrektheit und Vollständigkeit.

ZusammenfassungSignaturen und Algebren sind die beiden zentralen Abschnitte dieses Kapitels nach der konzeptuellen Einleitung. Signaturen bezeichnen das prinzipielle Format von Datenstrukturen, während der Begriff der Algebra die formale Entsprechung zum Begriff der Datenstruktur ist.

Umgangssprachlich bedeutet Kategorie soviel wie Art, Sorte oder Klasse, und in diesem Sinne wird auch der mathematische Begriff der Kategorie verstanden. Wie in der Einleitung diskutiert, dient die Einordnung von mathematischen Gegenständen in Kategorien dem strukturellen Vergleich dieser Gegenstände, und zwar sowohl im Bezug eines Objekts zu allen weiteren Objekten in der Kategorie als auch im Verhältnis der gesamten Kategorie zu anderen Kategorien. Eine entscheidende Rolle spielen dabei die Morphismen, die die möglichen Beziehungen zwischen den Objekten einer Kategorie darstellen.

ZusammenfassungUm Folgerungen maschinell zu beweisen, sind Hilbert-Kalküle und Sequenzenkalküle nicht gut geeignet, da sie nur schwer allgemeine Strategien zu formalisieren erlauben, die, von den gerade vorliegenden Formeln unabhängig, zu einer zielgerichteten Beweisführung beitragen. Eine besonders elegante Möglichkeit des Theorembeweisens bietet dagegen das Resolutionsverfahren, mit dem allgemeine Folgerungen von Formeln in konjunktiver Normalform bewiesen werden können.

According to the viewpoint model of software systems development abstract models of different views of the systems are constructed. This separation of concerns reduces the complexity of the development, but prompts the question for their integration, i.e., the conception of a collection of heterogeneous models as a complete specification of a system. The integration can be achieved by using a common semantic domain for the interpretation of all models, where each viewpoint model, due to its partiality, admits a set of possible interpretations. In this paper such an integrating semantic domain is sketched and an application to structure and behaviour models of the Unified Modeling Language is discussed.