Modal Transition Systems as the Basis for Interface Theories and Product Lines

This thesis presents research taking its outset in component-based software development, interface theory and software product lines, as well as modeling formalisms for describing component based software systems and their interfaces.
The main part of the thesis consists of five papers.
The first paper describes a framework for software product lines which can be instantiated for different design languages. Introducing the concept of color-blindness to describe the inability of an environment to distinguish the difference between several outputs, members of the software product line are automatically generated from a general model and the environment specifications.
The next two papers each present an extension of Interface Automata. The first of these papers define Interface I/O Automata an interface theory for the I/O Automata community. The main novelty compared to previous work is an explicit separation of assumptions from guarantees and the presentation of a formally derived composition operator.
The second of these papers present an interface theory combining Interface Automata and Modal Transition Systems into Modal I/O Automata. A formal correspondence between Interface Automata and a subset of modal transition systems is proved. The developed interface theory, which can describe liveness properties, is also applied as a behavioral variability theory for product line development.
The two last papers of the thesis concern themselves with modal and mixed transition systems. The first of these present and discuss four different forms of consistency. Algorithms for synthesizing implementations from a given consistency relation is described for all four consistencies.
The final paper proves PSPACE-hardness for common implementation and thorough refinement for mixed and modal transition systems. It also proves PSPACE-hardness for consistency of mixed specifications and establishes a number of reductions between the different decision problems.

Keywords:
Modeling, Software Product Lines, Embedded Software, Modal Refinement, Labeled Transition Systems, Modal Transition Systems, Mixed Transition Systems, Modal Specifications, Mixed Specifications, Interfaces, Interface Theory, Interface Automata, I/O automata, Modal I/O Automata, Behavioral Inequalities, Consistency, Common Implementation, Thorough Refinement, Operational Characterization, Synthesizing Implementations, Relativized Simulation