Return to search

Formal Analysis of Variability-Intensive and Context-Sensitive Systems

With the widespread use of information systems in modern society comes a growing demand for customizable and adaptable software. As a result, systems are increasingly developed as families of products adapted to specific contexts and requirements. Features are an established concept to capture the commonalities and variability between system variants. Most prominently, the concept is applied in the design, modeling, analysis, and implementation of software product lines where products are built upon a common base and are distinguished by their features. While adaptations encapsulated within features are mainly static and remain part of the system after deployment,
dynamic adaptations become increasingly important. Especially interconnected mobile devices and embedded systems are required to be context-sensitive and (self-)adaptive. A promising concept for the design and implementation of such systems are roles as they capture context-dependent and collaboration-specific behavior.

A major challenge in the development of feature-oriented and role-based systems are interactions, i.e., emergent behavior that arises from the combination of multiple features or roles. As the number of possible combinations is usually exponential in the number of features and roles, the detection of such interactions is difficult. Since unintended interactions may compromise the functional correctness of a system and may lead to reduced efficiency or reliability, it is desirable to detect them as early as possible in the
development process.

The goal of this thesis is to adopt the concepts of features and roles in the formal modeling and analysis of systems and system families. In particular, the focus is on the quantitative analysis of operational models by means of probabilistic model checking for supporting the development process and for ensuring correctness.

The tool ProFeat, which enables a quantitative analysis of stochastic system families defined in terms of features, has been extended with additional language constructs, support for a one-by-one analysis of system variants, and a symbolic representation of analysis results. The implementation is evaluated by means of several case studies which compare different analysis approaches and show how ProFeat facilitates a family-based quantitative analysis of systems.

For the compositional modeling of role-based systems, role-based automata (RBA) are introduced. The thesis presents a modeling language that is based on the input language of the probabilistic model checker PRISM to compactly describe RBA. Accompanying tool support translates RBA models into the PRISM language to enable the formal analysis of functional and non-functional properties, including system dynamics, contextual changes, and interactions. Furthermore, an approach for a declarative and compositional definition of role coordinators based on the exogenous coordination language Reo is proposed. The adequacy of the RBA approach for detecting interactions within context-sensitive and adaptive systems is shown by several case studies.:1 Introduction
1.1 Engineering approaches for variant-rich adaptive systems
1.2 Validation and verification methods
1.3 Analysis of feature-oriented and role-based systems
1.4 Contribution
1.5 Outline

2 Preliminaries


I Feature-oriented systems

3 Feature-oriented engineering for family-based analysis
3.1 Feature-oriented development
3.2 Describing system families: The ProFeat language
3.2.1 Feature-oriented language constructs
3.2.2 Parametrization
3.2.3 Metaprogramming language extensions
3.2.4 Property specifications
3.2.5 Semantics
3.3 Implementation
3.3.1 Translation of ProFeat models
3.3.2 Post-processing of analysis results

4 Case studies and application areas
4.1 Comparing family-based and product-based analysis
4.1.1 Analysis of feature-oriented systems
4.1.2 Analysis of parametrized systems
4.2 Software product lines
4.2.1 Body sensor network
4.2.2 Elevator product line
4.3 Self-adaptive systems
4.3.1 Adaptive network system model
4.3.2 Adaptation protocol for distributed systems


II Role-based Systems

5 Formal modeling and analysis of role-based systems
5.1 The role concept
5.1.1 Towards a common notion of roles
5.1.2 The Compartment Role Object Model
5.1.3 Roles in programming languages
5.2 Compositional modeling of role-based behavior
5.2.1 Role-based automata and their composition
5.2.2 Algebraic properties of compositions
5.2.3 Coordination and semantics of RBA

6 Implementation of a role-oriented modeling language
6.1 Role-oriented modeling language
6.1.1 Declaration of the system structure
6.1.2 Definition of operational behavior
6.2 Translation of role-based models
6.2.1 Transformation to multi-action MDPs
6.2.2 Multi-action extension of PRISM
6.2.3 Translation of components
6.2.4 Translation of role-playing coordinators
6.2.5 Encoding role-playing into states

7 Exogenous coordination of roles
7.1 The exogenous coordination language Reo
7.2 Constraint automata
7.3 Embedding of role-based automata in constraint automata
7.4 Implementation
7.4.1 Exogenous coordination of PRISM modules
7.4.2 Reo for exogenous coordination within PRISM

8 Evaluation of the role-oriented approach
8.1 Experimental studies
8.1.1 Peer-to-peer file transfer
8.1.2 Self-adaptive production cell
8.1.3 File transfer with exogenous coordination
8.2 Classification
8.3 Related work
8.3.1 Role-based approaches
8.3.2 Aspect-oriented approaches
8.3.3 Feature-oriented approaches


9 Conclusion

Identiferoai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:73691
Date29 January 2021
CreatorsChrszon, Philipp
ContributorsBaier, Christel, Boer, Frank S. de, Technische Universität Dresden
Source SetsHochschulschriftenserver (HSSS) der SLUB Dresden
LanguageEnglish
Detected LanguageEnglish
Typeinfo:eu-repo/semantics/publishedVersion, doc-type:doctoralThesis, info:eu-repo/semantics/doctoralThesis, doc-type:Text
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0021 seconds