product iamge

Composing Model-Based Analysis Tools

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Download
Search on Amazon

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

This book presents joint works of members of the software engineering and formal methods communities with representatives from industry, with the goal of establishing the foundations for a common understanding of the needs for more flexibility in model-driven engineering. It is based on the Dagstuhl Seminar 19481 „Composing Model-Based Analysis Tools“, which was held November 24 to 29, 2019, at Schloss Dagstuhl, Germany, where current challenges, their background and concepts to address them were discussed.

The book is structured in two parts, and organized around five fundamental core aspects of the subject: (1) the composition of languages, models and analyses; (2) the integration and orchestration of analysis tools; (3) the continual analysis of models; (4) the exploitation of results; and (5) the way to handle uncertainty in model-based developments. After a chapter on foundations and common terminology and a chapter on challenges in the field, one chapter is devoted to each of the above five core aspects in the first part of the book. These core chapters are accompanied by additional case studies in the second part of the book, in which specific tools and experiences are presented in more detail to illustrate the concepts and ideas previously introduced.

The book mainly targets researchers in the fields of software engineering and formal methods as well as software engineers from industry with basic familiarity with quality properties, model-driven engineering and analysis tools. From reading the book, researchers will receive an overview of the state-of-the-art and current challenges, research directions, and recent concepts, while practitioners will be interested to learn about concrete tools and practical applications in the context of case studies.

Author(s): Robert Heinrich, Francisco Durán, Carolyn Talcott, Steffen Zschaler
Publisher: Springer
Year: 2021

Language: English
Pages: 323
City: Cham

Foreword by Jeff Gray
Foreword by Antonio Vallecillo
Preface
Contents
Contributors
1 Introduction
1.1 Motivation and Context
1.2 Goals of the Book
1.3 Target Audience
1.4 Structure of the Book
1.5 How to Read This Book
References
2 Foundations
2.1 Models, Modelling Languages, and Their Composition
2.1.1 Types of Models and Their Role in Analysis
2.1.2 What Is a Modelling Language?
2.1.3 Metamodels
2.1.4 Property Models
2.1.5 Two Dimensions of Model Compositionality
2.1.6 Models of Context
2.1.7 Model and Language Composition
2.1.8 Model Transformations and Transformation Models
2.2 Analysis and Analysis Composition
2.2.1 Automation Degree
2.2.2 Design Time vs. Runtime Analyses
2.2.3 Quantitative vs. Qualitative Analyses
2.2.4 Purpose of Analysis
2.2.5 Correction and Counterexamples
2.2.6 Quality of Analyses
2.2.7 Analysis Composition
References
Part I Challenges and Concepts
3 Overview of Challenges in Composing Model-BasedAnalysis Tools
Reference
4 Composition of Languages, Models, and Analyses
4.1 Introduction and Problem Statement
4.2 Brief Overview of Models and Their Composition
4.3 Brief Overview of Analysis
4.4 What Is Composition?
4.4.1 Targets of Composition
4.4.2 Forms of Composition
4.5 Mathematical Characterisation
4.5.1 Model
4.5.2 Analysis
4.5.3 Composition
Simple Result Composition
Model Decomposition and Result Composition
Sequential Composition
Mutually Improving Analysis Composition
Simulation Composition
4.5.4 Composition of Contexts
4.5.5 Compositionality of Property Satisfaction
4.6 Examples
4.6.1 Rewriting Logic and Its Realisation in the Maude Language and System
4.6.2 Abstract State Machines and the ASMETA Analysis Toolset
4.6.3 Palladio
4.6.4 Hybrid Automata
4.6.5 The GEMOC Studio and BCOoL
4.7 Conclusion and Outlook
References
5 Integration and Orchestration of Analysis Tools
5.1 Introduction
5.2 Context and Problem Statement
5.3 State of the Art
5.3.1 Research on Integrating and Orchestrating Tools
5.3.2 Examples of Modelling Environments with Integrated Analysis Tools
5.4 A Reference Architecture for Integrating Analysis Tools
5.5 Requirements for Analysis Tool Integration and Orchestration
5.5.1 Integration Requirements
5.5.2 Orchestration Requirements
5.6 Orchestration Strategies
5.6.1 Orchestration Strategy Overview
5.6.2 Orchestration Strategy Definition
5.7 Examples of Orchestration Strategy Application
5.8 Conclusion and Outlook
References
6 Continual Model-Based Analysis
6.1 Introduction
6.2 Algebraic Specification of the Continual Model-Based Analysis Framework
6.2.1 Descriptive Models of the System
6.2.2 Structural, Behavioural, and Quality Models
6.2.3 Domain-Specific Requirements
6.2.4 Model-Based Analysis
Model Checking
Probabilistic Model Checking
Model-Based Safety Analysis
6.2.5 Composition Model-Based Analysis and Results Reuse
6.2.6 Summary
6.3 Incremental Verification of Service-Based Systems
6.3.1 Component Models
6.3.2 Probabilistic Automatons for SBSs
6.3.3 Assume-Guarantee Model Checking of SBSs
6.3.4 Verification Tasks
6.3.5 Incremental Verification
6.3.6 Change Scenarios
Server Hard-Disk Failure
Server Memory Upgrade
Adding New Functionality Components
Removing Deployed Functionality
6.3.7 Summary
6.4 Continuous Analysis of Safety-Critical Systems
6.4.1 Instantiation of the CMBA for Safety-Critical Systems Development
6.4.2 Change Scenarios
6.5 Business Processes
6.5.1 Background
6.5.2 Business Processes: Order2Cash and Procure2Pay
6.5.3 Opportunities for Continual Model-Based Analysis
6.5.4 Instantiation of the CMBA for Business Processes
6.5.5 Change Scenarios
6.6 Composition of CMBA Frameworks
6.6.1 Logical Deployment Configuration Models
6.6.2 Reliability Analysis of Satisfiable Deployment Configurations
6.7 Conclusion
References
7 Exploiting Results of Model-Based Analysis Tools
7.1 Introduction
7.2 A General Model of Results Exploitation
7.3 A Feature Model of Results-Exploitation Approaches
7.4 Example Cases
7.4.1 Soundness and Safeness of Business Processes
7.4.2 Analysis of API Usage
7.4.3 Diversity-Aware Model Finding with USE
7.4.4 Novice Programmer Errors
7.4.5 Design Smells Detection
7.4.6 Visual-Based Identification of Object-Churn Sources
7.4.7 Change Impact Analysis
7.4.8 ATL Transformations
7.4.9 Counterexample-Guided Abstraction Refinement
7.4.10 Summary of Example Cases
7.5 Conclusions
References
8 Living with Uncertainty in Model-Based Development
8.1 Introduction
8.2 Uncertainty and Composition of Models
8.3 Software System Modelling
8.4 Model-Based Performance Analysis
8.5 Discussion of Challenges
8.6 Related Work
8.7 Conclusion
References
Part II Case Studies
9 GTSMorpher: Safely Composing Behavioural Analyses Using Structured Operational Semantics
9.1 Introduction
9.2 Motivating Example
9.3 The GTSMorpher Tool
9.3.1 Specifying GTS Morphisms
Basic GTS Syntax
Basic Morphism Syntax
Morphism Auto-Completion and Unique Auto-Completion
Mapping with Virtual Rules
9.3.2 GTS Families
9.3.3 GTS Amalgamation
9.4 An Application Example
9.4.1 Making PLS Taintable
9.4.2 Adding Taint Propagation
The KAMP GTS Family
Instantiating the Propagation Rules
9.4.3 The Final Taint-Propagating PLS
9.5 Conclusions and Outlook
References
10 Compositional Modelling Languages with Analytics and Construction Infrastructures Based on Object-Oriented Techniques—The MontiCore Approach
10.1 Introduction
10.2 Preliminaries
10.3 Compositional Language Engineering
10.3.1 Modular Syntax Definition
10.3.2 Modular Analysis Infrastructure
10.3.3 Composed Analyses
10.4 Related Work
10.5 Discussion
10.6 Conclusion
References
11 Challenges in the Evolution of Palladio—Refactoring Design Smells in a Historically-Grown Approach to Software Architecture Analysis
11.1 Introduction and Problem Statement
11.2 Overview of the Palladio-Bench
11.3 Design Smells in the Palladio Component Model
11.4 Design Smells in the Simulators
11.5 Decomposition and Composition Techniques
11.5.1 Decomposition and Composition of the Palladio Component Model
A Layered Reference Architecture for Metamodels
Refactoring Metamodel Design Smells
11.5.2 Decomposition and Composition of the Simulators
IntBIIS
PCA
OMPCM
Refactoring Simulator Design Smells
11.6 Conclusion and Outlook
References
12 AnATLyzer: Static Analysis of ATL Model Transformations
12.1 Introduction and Problem Statement
12.2 Background on ATL
12.3 Analysing and Fixing Model Transformations
12.3.1 Transformation Analysis
12.3.2 Quick-Fixing ATL Transformations
12.4 Tool Support
12.5 Building Transformations with AnATLyzer in Practice
12.5.1 Models and Packages
12.5.2 Packages and Classes
12.5.3 Fixing and Evolving the Transformation
12.6 Related Work
12.7 Conclusion and Outlook
References
13 Using Afra in Different Domains by Tool Orchestration
13.1 Introduction
13.2 Reactive Object Language (Rebeca)
13.3 Afra
13.4 PTRebeca Model Checking: Sequential Analysis Orchestration
13.5 Schedulability Analysis and Optimisation: Cooperating Analysis Orchestration
13.6 Flow Management: Nested Analysis Orchestrations
13.7 Safe Scenarios for Volvo CE Simulator: Sequential Analysis Orchestration
13.8 Conclusion
References
14 Conclusion
14.1 Summary
14.2 Research Roadmap
References