### Abstract

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

Original language | English |
---|

Place of Publication | Aalborg |
---|---|

Publisher | Aalborg Universitet |

Publication status | Published - 2008 |

Series | Ph.D. thesis |
---|---|

Number | 45 |

ISSN | 1601-0590 |

### Fingerprint

### Keywords

- Modeling
- Software Product Lines
- embedded software
- Modal Refinement
- Labelled 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

### Cite this

*Modal Transition Systems as the Basis for Interface Theories and Product Lines*. Aalborg: Aalborg Universitet. Ph.D. thesis, No. 45

}

*Modal Transition Systems as the Basis for Interface Theories and Product Lines*. Ph.D. thesis, no. 45, Aalborg Universitet, Aalborg.

**Modal Transition Systems as the Basis for Interface Theories and Product Lines.** / Nyman, Ulrik.

Research output: Book/Report › Ph.D. thesis › Research

TY - BOOK

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

AU - Nyman, Ulrik

PY - 2008

Y1 - 2008

N2 - 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

AB - 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

KW - Modellering

KW - software produkt familier

KW - indlejret software

KW - modal rafinering

KW - mærkede transitions systemer

KW - modale transitions systemer

KW - blandede transitions systemer

KW - modale specifikationer

KW - blandede specifikationer

KW - grænseflader

KW - grænseflade teori

KW - grænseflade automater

KW - I/O automater

KW - modale I/O automater

KW - opførselsmæssige uligheder

KW - konsistens

KW - fælles implementation

KW - grundig raffinering

KW - operationel karakteristik

KW - syntesering af implementationer

KW - relativiseret simulation

KW - Modeling

KW - Software Product Lines

KW - embedded software

KW - Modal Refinement

KW - Labelled Transition Systems

KW - Modal Transition Systems

KW - Mixed Transition Systems

KW - Modal Specifications

KW - Mixed Specifications

KW - Interfaces

KW - Interface Theory

KW - Interface Automata

KW - I/O Automata

KW - Modal I/O Automata

KW - Behavioral Inequalities

KW - Consistency

KW - Common Implementation

KW - Thorough Refinement

KW - Operational Characterization

KW - Synthesizing Implementations

KW - Relativized Simulation

M3 - Ph.D. thesis

T3 - Ph.D. thesis

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

PB - Aalborg Universitet

CY - Aalborg

ER -