Introduction
Organization
Contents – Part II
Programming - What is Next: The Role of Documentation
Discussing the Future Role of Documentation in the Context of Modern Software Engineering (ISoLA 2022 Track Introduction)
1 Motivation and Background
2 Contributions
2.1 Session 1: Duality Between Documentation and Code
2.2 Session 2: Synergies Between Documentation and Code
2.3 Session 3: Executable Documentation
References
Software System Documentation: Coherent Description of Software System Properties
1 Software System Documentation – for Whom and Why
2 Properties of Software Systems and Their Documentation
3 Documentation in System Development and Evolution
3.1 From Abstract Ideas to Design and Implementation
3.2 The Significance of Understanding
3.3 Requirements Management
3.4 Documentation, Validation, and Verification
3.5 Avoiding Outdated Documentation
3.6 Artefact Modelling
3.7 Rationale
3.8 Abstraction, Modularity, Encapsulation, and Information Hiding
3.9 Documentation in DevOps
4 Documentation via Modelling
4.1 Specification of Functionality
4.2 Architecture Documentation
4.3 Correctness of Documentations
4.4 Documenting Physical Systems
4.5 Integrated Documentation – Semantic Coherence
5 Conclusion
References
Models as Documents, Documents as Models
1 Introduction
2 The Purposes of Software Modelling
3 The Purposes of Software Documentation
4 What Counts as a Model?
5 What Counts as a Document?
6 Models as Documents
7 Documents as Models
8 Conclusions
References
Using Supplementary Properties to Reduce the Need for Documentation
1 Introduction
2 The Limitations of Abstraction Mechanisms
2.1 Classification and the Class Mechanism
2.2 Limitations in Describing Concurrent Processes
2.3 Mechanisms for Describing Architecture of Systems
2.4 Representative/Non-representative Aspects/Parts of Programs
3 The Essentials of Supplementary Properties
3.1 Accessing Global Variables
3.2 Enforcing Interface Restrictions
3.3 Provided and Required Properties
4 Details of qBeta and Supplementary Properties
4.1 Explaining qBeta
4.2 Supplementary Properties
4.3 The Immutable Supplementary Property
4.4 The Globals Property
4.5 The Interface Property
4.6 The Signature Property
4.7 qBeta Modules
4.8 The %Visible Property
4.9 The Requires Property
5 Related Work
6 Discussion
References
Pragmatics Twelve Years Later: A Report on Lingua Franca
1 Introduction
1.1 Contributions and Outline
2 Pragmatics in Linguistics and Modeling
3 Diagrams for Development of Lingua Franca Programs
3.1 Data Dependencies
3.2 Control Dependencies
4 On the Graphical Syntax in Lingua Franca
5 Auto-Layout of Lingua Franca Diagrams
6 Diagram Synthesis Tooling
7 Modeling Pragmatics—Obstacles, Opportunities and Outlook
7.1 A Priori User Concerns
7.2 Feedback After Usage and Lessons Learned
7.3 A Short Experience Report from the Railway Domain
7.4 The Challenges Ahead
8 Related Work
9 Summary and Conclusions
References
Assurance Provenance: The Next Challenge in Software Documentation
1 Introduction
2 Paradigm for Assured Software
2.1 Artifacts and Organization
2.2 Observations
2.3 Use Case for CAID: Maintaining Assurance Provenance
3 Related Work
4 CAID: A Vision for a Next Generation Development Tool Environment
4.1 Proof of Concept Prototype for CAID
4.2 A Draft Use Case: AUV Control
5 Conclusions
References
Formalization of the AADL Run-Time Services
1 Introduction
2 AADL Background
3 AADL Semantic Documentation Impact
3.1 Stakeholders
3.2 AADL Ecosystem Synchronization
4 Concepts
5 Static Semantics
6 Threads
6.1 Value Domains and Port Queues
6.2 Thread State
6.3 Dispatch Status RTS
6.4 Port RTS
6.5 Thread Entry Points
7 Director
7.1 System State
8 Communication
9 Example Traces
10 Related Work
11 Conclusion
References
Executable Documentation: Test-First in Action
1 Introduction
2 Related Work
3 Executable Documentation in Textual Programming
3.1 Test-Driven Executable Documentation
3.2 Instantaneous Views
3.3 Executable Documentation in Teaching
3.4 Executable Documentation Extensions
3.5 Individual Test Case Generation
4 Executable Documentation in Visual Programming
4.1 Web Template Language Issues
4.2 State-Evaluating WYSIWYG GUI Designer
5 Conclusion
References
Runtime Verification as Documentation
1 Introduction
2 State Reconstruction with Python
2.1 Robot Tracking Example
2.2 Other Examples from Industrial Practice
3 Visualization with PyContract
3.1 The Boolean Verdict Monitor
3.2 Augmenting the Boolean Verdict Monitor for Visualization
4 Timing Debugging with Nfer
5 Conclusion
References
Executable Documentation: From Documentation Languages to Purpose-Specific Languages
1 Introduction
2 Traditional Software Documentation
3 Language-Driven Engineering
3.1 DIME
3.2 EquinOCS
3.3 Documentation in Language-Driven Engineering
4 The DevOps Perspective
4.1 Continuous Integration and Deployment
4.2 Executable Documentation in Practice
5 Discussion
6 Conclusion
References
Automated Software Re-engineering
Automating Software Re-engineering: Introduction to the ISoLA 2022 Track
1 Introduction
2 The Track
3 The Papers
3.1 Models and Meta-models
3.2 Verification and Testing
3.3 Security and Privacy
References
A Consolidated View on Specification Languages for Data Analysis Workflows
1 Introduction
2 The Components of Data Analysis Workflows and Their Relations
2.1 Task
2.2 Interconnection
3 A Metamodel of Data Analysis Workflow Languages
4 Mapping of the Consolidated View to a Specific Workflow Language: Airflow
5 Conclusion and Discussion
References
A Systematic Approach for Interfacing Component-Based Software with an Active Automata Learning Tool
1 Introduction
2 Background
3 Active Automata Learning Framework
4 Interfacing Protocol
4.1 Software Architecture and Communication Patterns
4.2 Mapping Communication Patterns to Inputs/Outputs
4.3 The Interfacing Protocol and Its Responsibilities
4.4 Systematic Derivation of the Interfacing Protocol
4.5 Interfacing Protocol Optimization
5 Application
6 Conclusions and Future Work
References
Verified Software Units for Simple DFA Modules and Objects in C
1 Introduction
2 High-Level Overview of Verifiable C
3 Specifying and Verifying a Single Static DFA Module
4 Statically Allocated DFA Objects
4.1 Specification of the Statically Allocated Objects
4.2 Verification of Static-Object Implementations
5 Dynamically Allocated DFA Objects
6 Towards Semantic Subtyping
7 Putting It All Together
8 Discussion
References
A Notion of Equivalence for Refactorings with Abstract Execution
1 Introduction
2 Preliminaries
2.1 Abstract Execution
2.2 Proving Refactoring Correctness with Abstract Execution
3 Challenges in Complex Refactorings
3.1 Encoding the Hide Delegate refactoring
3.2 Object Creation
4 Potential Future Improvements
4.1 Trace Properties
4.2 Relational Invariants
5 Discussion
6 Related Work
7 Conclusion
References
Towards a Usable and Sustainable Deductive Verification Tool
1 Introduction
2 The Verification Tool KeY
3 Requirements on a Verification Tool
3.1 Targeted User Group
3.2 Objectives
3.3 Research Tasks
4 A Work Program
4.1 User Experience
4.2 Robustness
4.3 Adaptability
4.4 Community, Infrastructure
5 Related Work
6 Conclusion
References
On Technical Debt in Software Testing - Observations from Industry
1 Introduction
2 Background - Telecommunication Domain
3 Test Automation in Industry
4 Test Design Technologies
5 CI/CD - Build, Test and Regression Testing
6 System and Non-functional Testing
7 Test Maintenance
8 Fault-Fixing Loops
9 Test Tools and Test Environments
10 Quality Assurance
11 Knowledge and Skills in Testing
12 Management
13 Visions on Test in the Future
14 Method Used, Threats of Validity and Disclaimers
15 Conclusions
References
Refactoring Solidity Smart Contracts to Protect Against Reentrancy Exploits
1 Introduction
2 Background
2.1 Blockchain
2.2 Ethereum and Smart Contracts
2.3 The call() function
2.4 Reentrancy Exploit
2.5 The transfer() and send() Functions
2.6 The require(), assert() and revert() Functions
2.7 Static Analysis and Formal Verification
3 Research Questions
4 RQ1: Adoption of Safe Code Patterns
5 RQ2: SMTChecker for Safe Code Refactorings
5.1 Checks-Effects-Interactions
5.2 Mutex
6 Related Work
6.1 Static Analysis Tools
6.2 Verification Tools
6.3 Datasets
7 Conclusion
References
A Refactoring for Data Minimisation Using Formal Verification
1 Introduction
2 Background on Quantitative Information Flow
3 Formalisation
3.1 Programs and Fact Bases
3.2 Data Minimisation
3.3 Limitations
4 Data Minimisation Using Formal Verification
4.1 Front End: Finding Facts
4.2 Front End: Minimising Fact Sets
4.3 Back End: Computing the Result from a Fact Set
5 Implementation and Experiments
5.1 Prototypical Implementation
5.2 Example: Account Charges
6 Related Work
7 Conclusion
References
DIME Days
DIME Days (ISoLA 2022 Track Introduction)
1 Introduction
2 Contributions
2.1 Numbers on the Effect of Graphical Modeling
2.2 Quality Control in the LDE Ecosystem
2.3 Language-Driven Engineering in the Web
3 Outlook
References
Evaluation of Graphical Modeling of CI/CD Workflows with Rig
1 Introduction
2 Background
3 Research Questions
4 Workshop
4.1 Setup
4.2 Exercises
5 Results
6 Interpretation
7 Threats to Validity
8 Future Work
9 Conclusion
References
Towards Continuous Quality Control in the Context of Language-Driven Engineering
1 Introduction
2 Static Validation
2.1 Exploiting the Verifiability
2.2 Exploiting the Rigidity
3 Dynamic Validation
3.1 Learning-Based Testing
3.2 Lifelong Learning
3.3 Automation
4 Scalability
4.1 Meta-level Hierarchy
4.2 Path-up Effects
4.3 Tree-down Effects
5 Conclusion and Future Work
5.1 Design for Learnability
5.2 LDE in the Cloud
References
Cinco Cloud: A Holistic Approach for Web-Based Language-Driven Engineering
1 Introduction
2 Web-Based Cinco Editors and Products
2.1 Meta Layer
2.2 Modeling Layer
3 The Cloud Architecture of Cinco Cloud
3.1 Component Overview
3.2 Building Cinco Products in the Web
4 Example: WebStory in Cinco Cloud
4.1 Language Definition and IME Generation
4.2 Model Creation and Application Generation
4.3 Application Deployment
5 Related Approaches
5.1 WebGME
5.2 Sirius Web
5.3 emf.cloud
6 Conclusion and Future Work
6.1 Collaboration and Version Control
6.2 Model Evolution and Migration
References
Correction to: A Notion of Equivalence for Refactorings with Abstract Execution
Correction to: Chapter “A Notion of Equivalence for Refactorings with Abstract Execution” in: T. Margaria and B. Steffen (Eds.): Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering, LNCS 13702, https://doi.org/10.1007/978-3-031-19756-7_15
Author Index