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

Ulrik Nyman

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

Publikation: Ph.d.-afhandling

597 Downloads (Pure)

Abstract

Denne afhandling præsenterer forskning der tager udgangspunkt i komponentbaseret software udvikling, grænseflade teori og software produkt familier, så vel som modellerings formalismer beregnet til at beskrive komponentbaserede software systemer og deres grænseflader.

Hoveddelen af denne afhandling består af fem artikler.

Den første artikel beskriver en struktur for software produkt familier der kan instantieres for forskellige design sprog. Artiklen introducere konceptet farve blindhed (color-blindness) for at kunne beskrive en omgivelses manglende evne til at kunne skelne imellem forskellige output. Medlemmer af software produkt familien bliver automatisk genereret ud fra en general model og omgivelses beskrivelser.
De næste to artikler præsenterer hver en udvidelse af Interface Automata (grænseflade automater). Den første af disse to artikler definerer Interface I/O Automata (grænseflade I/O automater) en grænseflade teori for I/O Automater. Den væsentligste nyskabelse i forhold til tidligere teorier er en eksplicit adskillelse af antagelser fra garantier og at den præsenterer en formelt udledt kompositions operator.
Den anden af disse artikler præsenterer en grænseflade teori der kombinerer Interface Automata med Modale Transitions Systemer til Modal I/O Automata (modale I/O automater). Den indeholder også et bevis for en formal overensstemmelse mellem Interface Automata og en delmængde af modale transitions systemer. Denne grænseflade teori, der kan beskrive aktivitets (liveness) egeneskaber bliver også andvendt som en adfærdsmæssig variabilitets teori til software produkt familie udvikling.
De sidste to artikler omhandler modale og blandede transitions systemer. Den første artikel præsenterer og diskuterer fire forskellige former for konsistens. Algoritmer der kan syntetisere implementationer ud fra en given konsistens relation bliver beskrevet for alle fire konsistenser.
Den sidste artikel beviser PSPACE-hårdhed for fælles implementation (common implementation) og grundig raffinering (thorough refinement) for blandede og modale transitions systemer. Den viser også PSPACE-hårdhed for konsistens (consistency) for blandede specifikationer og fastslår en række reduktioner imellem de forskellige beslutnings problemer.

Nøgleord:
Modellering, software produkt familier, indlejret software, modal raffinering, mærkede transitions systemer, modale transition systemer, blandede transition systemer, modale specifikationer, blandede specifikationer, grænseflader, grænseflade teori, grænseflade automater, I/O automater, modale I/O automater, opførselsmæssige uligheder, konsistens, fælles implementation, grundig raffinering, operationel karakteristik, syntesering af implementationer, relativiseret simulation

Originalsprog	Engelsk
Udgivelsessted	Aalborg
Udgiver	Aalborg Universitet
Status	Udgivet - 2008

Emneord

Modellering
software produkt familier
indlejret software
modal rafinering
mærkede transitions systemer
modale transitions systemer
blandede transitions systemer
modale specifikationer
blandede specifikationer
grænseflader
grænseflade teori
grænseflade automater
I/O automater
modale I/O automater
opførselsmæssige uligheder
konsistens
fælles implementation
grundig raffinering
operationel karakteristik
syntesering af implementationer
relativiseret simulation

Adgang til dokumentet

UlrikNymanPhDThesisForlagets udgivne version, 1,52 MB

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Citationsformater

@misc{ab3ef840aa7111dd96a1000ea68e967b,

title = "Modal Transition Systems as the Basis for Interface Theories and Product Lines",

abstract = "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 ",

keywords = "Modellering, software produkt familier, indlejret software, modal rafinering, m{\ae}rkede transitions systemer, modale transitions systemer, blandede transitions systemer, modale specifikationer, blandede specifikationer, gr{\ae}nseflader, gr{\ae}nseflade teori, gr{\ae}nseflade automater, I/O automater, modale I/O automater, opf{\o}rselsm{\ae}ssige uligheder, konsistens, f{\ae}lles implementation, grundig raffinering, operationel karakteristik, syntesering af implementationer, relativiseret simulation, 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",

author = "Ulrik Nyman",

year = "2008",

language = "English",

series = "Ph.D. thesis",

publisher = "Aalborg Universitet",

number = "45",

}

TY - GEN

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 - PhD thesis

T3 - Ph.D. thesis

PB - Aalborg Universitet

CY - Aalborg

ER -

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

Abstract

Emneord

Adgang til dokumentet

AUB Link

Fingeraftryk

Citationsformater