Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part III / edited by Tiziana Margaria, Bernhard Steffen.

Format:

Book

Contributor:

Margaria, Tiziana, editor.

Steffen, Bernhard, editor.

Series:

Lecture Notes in Computer Science, 1611-3349 ; 13703

Language:

English

Subjects (All):

Software engineering.

Artificial intelligence.

Computer engineering.

Computer networks.

Microprogramming.

Computer science.

Software Engineering.

Artificial Intelligence.

Computer Engineering and Networks.

Control Structures and Microprogramming.

Theory of Computation.

Local Subjects:

Software Engineering.

Artificial Intelligence.

Computer Engineering and Networks.

Control Structures and Microprogramming.

Theory of Computation.

Physical Description:

1 online resource (483 pages)

Edition:

1st ed. 2022.

Place of Publication:

Cham : Springer Nature Switzerland : Imprint: Springer, 2022.

Summary:

This four-volume set LNCS 13701-13704 constitutes contributions of the associated events held at the 11th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2022, which took place in Rhodes, Greece, in October/November 2022. The contributions in the four-volume set are organized according to the following topical sections: specify this - bridging gaps between program specification paradigms; x-by-construction meets runtime verification; verification and validation of concurrent and distributed heterogeneous systems; programming - what is next: the role of documentation; automated software re-engineering; DIME day; rigorous engineering of collective adaptive systems; formal methods meet machine learning; digital twin engineering; digital thread in smart manufacturing; formal methods for distributed computing in future railway systems; industrial day.

Contents:

Intro

Introduction

Organization

Contents - Part III

Rigorous Engineering of Collective Adaptive Systems

Rigorous Engineering of Collective Adaptive Systems Introduction to the 4th Track Edition

1 Collective Adaptive Systems

2 Track Overview

3 Track Contributions

3.1 Design and Validation of Autonomous Systems

3.2 Computing with Bio-inspired Communication

3.3 New System Models and Tools for Ensembles

3.4 Large Ensembles and Collective Dynamics

3.5 Panel: On the Borderline Between Collective Stupidity and Collective Intelligence

3.6 Machine Learning for Collective Adaptive Systems

3.7 Programming and Analysing Ensembles

3.8 Tools for Formal Analysis and Design

References

Correct by Design Coordination of Autonomous Driving Systems

1 Introduction

2 Map Representation

3 The ADS Dynamic Model

3.1 General ADS Architecture

3.2 Assume-Guarantee for Safe Control Policies

4 Speed Policies Abiding by the Vehicle Contract

5 Free Space Policies Implied by Traffic Rules

5.1 Writing Specifications of Traffic Rules

5.2 Deriving Free Space Rules from Traffic Rules

5.3 Correctness with Respect to the Free Space Contract

6 Discussion

Neural Predictive Monitoring for Collective Adaptive Systems

2 Bike Sharing System

2.1 Model of the System

2.2 Dynamics of the System

3 Neural Predictive Monitoring for CAS

3.1 Deterministic Dynamics

3.2 Stochastic Dynamics

3.3 Predictive Monitoring for BSS

4 Uncertainty Quantification and Statistical Guarantees

4.1 Conformal Predictions for Multi-output and Multi-class Classification

4.2 Uncertainty-Based Rejection Rule

5 Experiments

5.1 Results

5.2 Discussion

6 Conclusions

An Extension of HybridSynchAADL and Its Application to Collaborating Autonomous UAVs.

1 Introduction

2 Preliminaries

3 Overview of HybridSynchAADL

3.1 The HybridSynchAADL Modeling Language

3.2 Symbolic Semantics of HybridSynchAADL

4 An Extension of HybridSynchAADL

5 Extending the Semantics of HybridSynchAADL

5.1 Representation of the Additional Features

5.2 Semantic of Composite Data Types

5.3 Semantics of Subprogram Calls

6 Case Study: A Packet Delivery System

6.1 System Description

6.2 The HybridSynchAADL Model

6.3 Formal Analysis

7 Related Work

8 Concluding Remarks

Discrete Models of Continuous Behavior of Collective Adaptive Systems

2 Running Example: Ants on a Bar

2.1 The Behavior of Ants on a Bar

2.2 Events of the Ants' System

3 Conventional Models of the Ants' Behavior

3.1 The Continuous Model of a Run of the Ants System

3.2 The Grid Model

3.3 The Numbering Model

3.4 The Lockstep Model

3.5 The Uniqueness Problem

3.6 Weak Orderings of Events

4 The Causal Model of the Ants' Runs

4.1 The Order of Events

4.2 Local States and Steps

4.3 The Run Starting at State S0

4.4 Composing the Run U from the Ants' Behavior

5 Modeling the Bar with Ants

5.1 The Model of the Ants System

5.2 Composing Two Bars

5.3 Composing Many Bars

6 A Schematic Representation of Ants Systems

8 Conclusion

Modelling Flocks of Birds from the Bottom Up

2 Specification

3 Simulation Results

4 Related Work

5 Conclusion

Towards Drone Flocking Using Relative Distance Measurements

2 Drone Flocking

2.1 What Is a Flock?

2.2 Cost Function

2.3 Flock-Formation Quality Metrics

3 Distributed Flocking Controller Using Relative Distances

3.1 Environmental Knowledge Representation

3.2 Distributed Flocking Controller.

4 Experiments

4.1 Simulation Experiments

4.2 Results

5 Related Work

Epistemic Ensembles

2 Epistemic Logic and Epistemic Actions

2.1 Epistemic Logic

2.2 Epistemic Actions

3 Epistemic Ensemble Specifications

4 Semantics of Epistemic Ensemble Specifications

5 Epistemic Ensemble Realisations

6 Conclusion

A Modal Approach to Consciousness of Agents

2 Conscious Agents

2.1 Agents

2.2 Actions

2.3 Features

2.4 Multiagent Systems

3 Appreciating Awareness

4 Soundness

5 Adaptivity

6 Related Work and Progress

An Experimental Toolchain for Strategy Synthesis with Spatial Properties

2 Background

2.1 CATLib, Automata Composition, and Strategy Synthesis

2.2 VoxLogicA, Spatial Model Checking, and Image Analysis

3 Tool Methodology

4 Experiments

Toward a Kinetic Framework to Model the Collective Dynamics of Multi-agent Systems

2 The Basis of the KTMAS Framework

3 The Case of the Symmetric Gossip Algorithm

3.1 Model

3.2 Analytic Results

4 Theory Vs. Simulations

Understanding Social Feedback in Biological Collectives with Smoothed Model Checking

1.1 Illustrative Example

2 Methods

2.1 Gaussian Process

2.2 Gaussian Process Regression

2.3 Gaussian Process Classification

2.4 Smoothed Model Checking

2.5 Model Selection

2.6 Problem Statement

3 Results

3.1 Data

3.2 Predict the Collective Response

3.3 Inferring the Fitness Function

4 Conclusion

Efficient Estimation of Agent Networks

2.1 Estimation of Agent Networks

2.2 Backward Differential Equivalence.

3 Efficient Estimation of Agent Networks

4 Evaluation

Attuning Adaptation Rules via a Rule-Specific Neural Network

2 Motivating Example

3 Refining Adaptation Rules

3.1 Atomic Attunable Predicates as rsNN Seeds

3.2 Making Guard Predicates Attunable

3.3 Construction of rsNN

3.4 Training an rsNN

Measuring Convergence Inertia: Online Learning in Self-adaptive Systems with Context Shifts

2 Background and Running Example

2.1 Online Learning in Self-adaptive Systems

2.2 Overview of Multi-armed Bandits

2.3 Running Example: SWIM

3 Dealing with Context Switches in Online Learning

4.1 Setup

5 Discussion

6 Related Work

7 Conclusion

Capturing Dependencies Within Machine Learning via a Formal Process Model

2 Background and Related Work

2.1 SE for (Self-)adaptive Systems

2.2 SE for ML Systems

2.3 Fundamental ML Challenges

3 A Process Model to Capture Dependencies Within ML

3.1 Visualization

3.2 Description of Activities

3.3 Proof of Concept

3.4 Formalization

4 Summary and Outlook

On Model-Based Performance Analysis of Collective Adaptive Systems

2 A Robot Scenario

3 A Behavioural Specification Model

3.1 Independent Architecture

3.2 Collaborative Architecture

4 Quantitative Analysis

4.1 Independent Architecture

4.2 Collaborative Architecture

6 Conclusions, Related and Future Work

Programming Multi-robot Systems with X-KLAIM

2 The X-Klaim Language

3 The X-Klaim Approach to Multi-robot Programming

4 The X-Klaim Approach at Work on an MRS Scenario.

5 Discussion and Related Work

6 Concluding Remarks and Future Work

Bringing Aggregate Programming Towards the Cloud

2.1 Aggregate Programming and the FCPP DSL

2.2 FCPP Library Architecture

2.3 Graph Statistics

3 Roadmap

4 A First Step: Extending FCPP to work with Graphs

5 Experimental Evaluation

5.1 Implementation

5.2 Results

6 Discussion and Conclusions

Ensemble-Based Modeling Abstractions for Modern Self-optimizing Systems

2 Running Example and Background

2.1 Modeling Dynamic Security Rules with Components and Ensembles

3 Estimates

3.1 Estimates

3.2 Training of the Estimates

4 Heuristics

5 Evaluation

Formal Analysis of Lending Pools in Decentralized Finance

2 Lending Pools and Price Models

3 An LP Simulator for Liquidating Agents

3.1 A Fully-Automated Liquidating Strategy

3.2 Price Modelling

4 Statistical Analysis of Liquidation Scenarios

5 Related Works

A Figures

A Rewriting Framework for Interacting Cyber-Physical Agents

2 Semantic Model: Algebra of Components

2.1 Components

2.2 Product and Division

3 System of Agents and Compositional Semantics

3.1 Action, Agent, and System

4 Application

4.1 General Framework

4.2 Analysis in Maude

Model Checking Reconfigurable Interacting Systems

2 ReCiPe: A Model of Computation

3 The R-CHECK Language

3.1 The Semantics of R-CHECK

4 Case Study: Autonomous Resource Allocation

5 Model-Checking Through nuXmv

6 Concluding Remarks

Formal Methods Meet Machine Learning

Formal Methods Meet Machine Learning (F3ML).

1 Preface.

Notes:

Includes bibliographical references and index.

ISBN:

9783031197598

3031197593

OCLC:

1348483213