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 / / Tiziana Margaria, Bernhard Steffen, editors

• Pubblicazione: Cham, Switzerland : , : Springer, , [2022]; ©2022
• Descrizione fisica: 1 online resource (483 pages)
• Disciplina: 005.14
• Soggetto topico: Computer software - Verification; Formal methods (Computer science)
• Persona (resp. second.): MargariaTiziana; SteffenBernhard
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: 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 -- References -- Neural Predictive Monitoring for Collective Adaptive Systems -- 1 Introduction -- 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 -- References -- 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 -- References -- Discrete Models of Continuous Behavior of Collective Adaptive Systems -- 1 Introduction -- 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 -- 7 Related Work -- 8 Conclusion -- References -- Modelling Flocks of Birds from the Bottom Up -- 1 Introduction -- 2 Specification -- 3 Simulation Results -- 4 Related Work -- 5 Conclusion -- References -- Towards Drone Flocking Using Relative Distance Measurements -- 1 Introduction -- 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 -- 6 Conclusions -- References -- Epistemic Ensembles -- 1 Introduction -- 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 -- References -- A Modal Approach to Consciousness of Agents -- 1 Introduction -- 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 -- References -- An Experimental Toolchain for Strategy Synthesis with Spatial Properties -- 1 Introduction -- 2 Background -- 2.1 CATLib, Automata Composition, and Strategy Synthesis -- 2.2 VoxLogicA, Spatial Model Checking, and Image Analysis -- 3 Tool Methodology -- 4 Experiments -- 5 Conclusion -- References -- Toward a Kinetic Framework to Model the Collective Dynamics of Multi-agent Systems -- 1 Introduction -- 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 -- 5 Related Work -- 6 Conclusion -- References -- Understanding Social Feedback in Biological Collectives with Smoothed Model Checking -- 1 Introduction -- 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 -- References -- Efficient Estimation of Agent Networks -- 1 Introduction -- 2 Preliminaries -- 2.1 Estimation of Agent Networks -- 2.2 Backward Differential Equivalence. ; 3 Efficient Estimation of Agent Networks -- 4 Evaluation -- 5 Conclusion -- References -- Attuning Adaptation Rules via a Rule-Specific Neural Network -- 1 Introduction -- 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 -- 4 Evaluation -- 5 Related Work -- 6 Conclusion -- References -- Measuring Convergence Inertia: Online Learning in Self-adaptive Systems with Context Shifts -- 1 Introduction -- 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 Experiments -- 4.1 Setup -- 4.2 Results -- 5 Discussion -- 6 Related Work -- 7 Conclusion -- References -- Capturing Dependencies Within Machine Learning via a Formal Process Model -- 1 Introduction -- 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 -- References -- On Model-Based Performance Analysis of Collective Adaptive Systems -- 1 Introduction -- 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 -- 5 Discussion -- 6 Conclusions, Related and Future Work -- References -- Programming Multi-robot Systems with X-KLAIM -- 1 Introduction -- 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 -- References -- Bringing Aggregate Programming Towards the Cloud -- 1 Introduction -- 2 Background -- 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 -- References -- Ensemble-Based Modeling Abstractions for Modern Self-optimizing Systems -- 1 Introduction -- 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 -- 6 Related Work -- 7 Conclusion -- References -- Formal Analysis of Lending Pools in Decentralized Finance -- 1 Introduction -- 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 -- 6 Conclusions -- A Figures -- References -- A Rewriting Framework for Interacting Cyber-Physical Agents -- 1 Introduction -- 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 -- 5 Related Work -- 6 Conclusion -- References -- Model Checking Reconfigurable Interacting Systems -- 1 Introduction -- 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 -- References -- Formal Methods Meet Machine Learning -- Formal Methods Meet Machine Learning (F3ML). ; 1 Preface.
• Titolo autorizzato: Leveraging applications of formal methods, verification and validation. Adaptation and learning
• ISBN: 3-031-19759-3
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910619267703321
• Lo trovi qui: Univ. Federico II
• Serie: Lecture notes in computer science ; ; 13703.