top

  Info

  • Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.
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
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
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2022]
Descrizione fisica 1 online resource (483 pages)
Disciplina 005.14
Collana Lecture notes in computer science
Soggetto topico Computer software - Verification
Formal methods (Computer science)
ISBN 3-031-19759-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
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.
Record Nr. UNINA-9910619267703321
Cham, Switzerland : , : Springer, , [2022]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
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
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
Pubbl/distr/stampa Cham, Switzerland : , : Springer, , [2022]
Descrizione fisica 1 online resource (483 pages)
Disciplina 005.14
Collana Lecture notes in computer science
Soggetto topico Computer software - Verification
Formal methods (Computer science)
ISBN 3-031-19759-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
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.
Record Nr. UNISA-996495569003316
Cham, Switzerland : , : Springer, , [2022]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems [[electronic resource] ] : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III / / edited by Tiziana Margaria, Bernhard Steffen
Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems [[electronic resource] ] : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III / / edited by Tiziana Margaria, Bernhard Steffen
Edizione [1st ed. 2018.]
Pubbl/distr/stampa Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Descrizione fisica 1 online resource (XIV, 522 p. 175 illus., 86 illus. in color.)
Disciplina 004.0151
Collana Theoretical Computer Science and General Issues
Soggetto topico Software engineering
Compilers (Computer programs)
Artificial intelligence
Computer science
Computer engineering
Computer networks
Computers
Professions
Software Engineering
Compilers and Interpreters
Artificial Intelligence
Theory of Computation
Computer Engineering and Networks
The Computing Profession
ISBN 3-030-03424-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Rigorous Engineering of Collective Adaptive Systems - Introduction to the 2nd Track Edition -- DReAM: Dynamic Reconfigurable Architecture Modeling -- Dynamic Logic for Ensembles -- Modelling the Transition to Distributed Ledgers -- Collective Adaptive Socio-Technical System for Remote- and Self-Supervised Exercise in the Treatment of Intermittent Claudication -- Engineering Collectives of Self-driving Vehicles: the SOTA Approach -- Synthesizing Capabilities for Collective Adaptive Systems from Self-Descriptive Hardware Devices – Bridging the Reality Gap -- The Meaning of Adaptation: Mastering the Unforeseen? -- Mutation-based Test Suite Evolution For Self-Organizing Systems -- Adapting Quality Assurance to Adaptive Systems: The Scenario Coevolution Paradigm -- Designing Systems with Detection and Reconfiguration Capabilities: A Formal Approach -- Dynamic Security Specification through Autonomic Component Ensembles -- Differential Equivalence yields Network Centrality -- Measuring and Evaluating the Performance of Self-Organization Mechanisms within Collective Adaptive Systems -- Engineering Sustainable and Adaptive Systems in Dynamic Environments -- The Sharer's Dilemma in Collective Adaptive Systems of Self-Interested Agents -- Coordination model with reinforcement learning for ensuring reliable on-demand services in collective adaptive systems -- Data-driven modelling and simulation of urban transportation systems using Carma -- GoAt: Attribute-based Interaction in Google Go -- Four Exercises in Programming Dynamic Reconfigurable Systems: Methodology and Solution in DR-BIP -- ISoLA 2018 - Verification and Validation of Distributed Systems: Track Introduction -- ByMC: Byzantine Model Checker -- Static code verification through process models -- Effective Test Suite Design for Detecting Concurrency Control Faults in Distributed Transaction Systems -- Towards automated testing of the Internet of Things: Results obtained with the TESTAR tool -- Quantitative Safety Analysis of a Coordinated Emergency Brake Protocol for Vehicle Platoons -- Cyber-Physical Systems Engineering: An Introduction -- Intelligent Adaption Process in Cyber-Physical Production Systems (CPPS) -- Model-Based Systems Engineering for Systems Simulation -- Scenario-based validation of automated driving systems -- Engineering of Cyber-Physical Systems in the automotive context: case study of a range prediction assistant -- Testing Avionics Software: Is FMI up to the Task? -- Lessons Learned Using FMI Co-Simulation for Model-based Design of Cyber Physical Systems -- Co-simulation: the Past, Future, and Open Challenges.
Record Nr. UNISA-996466452403316
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III / / edited by Tiziana Margaria, Bernhard Steffen
Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part III / / edited by Tiziana Margaria, Bernhard Steffen
Edizione [1st ed. 2018.]
Pubbl/distr/stampa Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Descrizione fisica 1 online resource (XIV, 522 p. 175 illus., 86 illus. in color.)
Disciplina 004.0151
Collana Theoretical Computer Science and General Issues
Soggetto topico Software engineering
Compilers (Computer programs)
Artificial intelligence
Computer science
Computer engineering
Computer networks
Computers
Professions
Software Engineering
Compilers and Interpreters
Artificial Intelligence
Theory of Computation
Computer Engineering and Networks
The Computing Profession
ISBN 3-030-03424-0
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Rigorous Engineering of Collective Adaptive Systems - Introduction to the 2nd Track Edition -- DReAM: Dynamic Reconfigurable Architecture Modeling -- Dynamic Logic for Ensembles -- Modelling the Transition to Distributed Ledgers -- Collective Adaptive Socio-Technical System for Remote- and Self-Supervised Exercise in the Treatment of Intermittent Claudication -- Engineering Collectives of Self-driving Vehicles: the SOTA Approach -- Synthesizing Capabilities for Collective Adaptive Systems from Self-Descriptive Hardware Devices – Bridging the Reality Gap -- The Meaning of Adaptation: Mastering the Unforeseen? -- Mutation-based Test Suite Evolution For Self-Organizing Systems -- Adapting Quality Assurance to Adaptive Systems: The Scenario Coevolution Paradigm -- Designing Systems with Detection and Reconfiguration Capabilities: A Formal Approach -- Dynamic Security Specification through Autonomic Component Ensembles -- Differential Equivalence yields Network Centrality -- Measuring and Evaluating the Performance of Self-Organization Mechanisms within Collective Adaptive Systems -- Engineering Sustainable and Adaptive Systems in Dynamic Environments -- The Sharer's Dilemma in Collective Adaptive Systems of Self-Interested Agents -- Coordination model with reinforcement learning for ensuring reliable on-demand services in collective adaptive systems -- Data-driven modelling and simulation of urban transportation systems using Carma -- GoAt: Attribute-based Interaction in Google Go -- Four Exercises in Programming Dynamic Reconfigurable Systems: Methodology and Solution in DR-BIP -- ISoLA 2018 - Verification and Validation of Distributed Systems: Track Introduction -- ByMC: Byzantine Model Checker -- Static code verification through process models -- Effective Test Suite Design for Detecting Concurrency Control Faults in Distributed Transaction Systems -- Towards automated testing of the Internet of Things: Results obtained with the TESTAR tool -- Quantitative Safety Analysis of a Coordinated Emergency Brake Protocol for Vehicle Platoons -- Cyber-Physical Systems Engineering: An Introduction -- Intelligent Adaption Process in Cyber-Physical Production Systems (CPPS) -- Model-Based Systems Engineering for Systems Simulation -- Scenario-based validation of automated driving systems -- Engineering of Cyber-Physical Systems in the automotive context: case study of a range prediction assistant -- Testing Avionics Software: Is FMI up to the Task? -- Lessons Learned Using FMI Co-Simulation for Model-based Design of Cyber Physical Systems -- Co-simulation: the Past, Future, and Open Challenges.
Record Nr. UNINA-9910349396803321
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice [[electronic resource] ] : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV / / edited by Tiziana Margaria, Bernhard Steffen
Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice [[electronic resource] ] : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV / / edited by Tiziana Margaria, Bernhard Steffen
Edizione [1st ed. 2018.]
Pubbl/distr/stampa Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Descrizione fisica 1 online resource (XIV, 530 p. 363 illus., 250 illus. in color.)
Disciplina 004.0151
Collana Theoretical Computer Science and General Issues
Soggetto topico Software engineering
Compilers (Computer programs)
Artificial intelligence
Computer science
Computer engineering
Computer networks
Computers
Professions
Software Engineering
Compilers and Interpreters
Artificial Intelligence
Theory of Computation
Computer Engineering and Networks
The Computing Profession
ISBN 3-030-03427-5
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto RV-TheToP: Runtime Verification from the Theory To the industry Practice (Track Introduction) -- Opportunities and Challenges in Monitoring Cyber-physical Systems Security -- Migrating Monitors + ABE: A Suitable Combination for Secure IoT? -- Capturing Inter-Process Communication for Runtime Verification on Android -- Considering Academia-Industry Projects Meta-Characteristics in Runtime Verification Design -- Flexible Monitor Deployment for Runtime Verification of Large Scale Software -- Increasing the Reusability of Enforcers with Lifecycle Events -- BDDs on the Run -- Verifying Real-World Software with Contracts for Concurrency -- Formal Methods in Industrial Practice - bridging the gap (Track Summary) -- Model-based Testing for Avionic Systems -- Proven Benefits and Further Challenges -- Test Case Generation with PathCrawler/LTest: How to Automate an Industrial Testing Process -- Pitfalls in Applying Model Learning to Industrial Legacy Software -- Formal Verification in Automotive Industry: Enablers and Obstacles -- Scalability of Deductive Verification Depends on Method Call Treatment -- Java Automated Deductive Verification in Practice: Lessons from industrial proof-based projects -- Security Filters for IoT Domain Isolation -- 20 Years of Uppaal Enabled Industrial Model-Based Validation and Beyond -- Verification of Operating System Monolithic Kernels without Extensions -- A Proposal of an Example and Experiments Repository to Foster Industrial Adoption of Formal Methods -- Reliable Smart Contracts: State-of-the-art, Applications, Challenges and Future Directions -- Smart Contracts and Opportunities for Formal Methods -- Contracts over Smart Contracts: Recovering from Violations Dynamically -- Security Analysis of Smart Contracts in Datalog -- Temporal Properties of Smart Contracts -- Temporal Aspects of Smart Contracts for Financial Derivatives -- Marlowe: financial contracts on blockchain -- SMT-based Verification of Solidity Smart Contracts -- Blockchains as Kripke Models: an Analysis of Atomic Cross-Chain Swap -- A Language-Independent Approach To Smart Contract Verification -- Towards Adding Variety to Simplicity -- Fun with Bitcoin smart contracts -- Computing Exact Worst-Case Gas Consumption for Smart Contracts -- Digital Transformation Trends: Industry 4.0, Automation, and AI -- A Methodology for Combinatory Process Synthesis: Process Variability in Clinical Pathways -- Automatic composition of rough solution possibilities in the target planning of factory planning projects by means of combinatory logic -- GOLD: Global Organization aLignment and Decision - Towards the Hierarchical Integration of Heterogeneous Business Models.
Record Nr. UNISA-996466452503316
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV / / edited by Tiziana Margaria, Bernhard Steffen
Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV / / edited by Tiziana Margaria, Bernhard Steffen
Edizione [1st ed. 2018.]
Pubbl/distr/stampa Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Descrizione fisica 1 online resource (XIV, 530 p. 363 illus., 250 illus. in color.)
Disciplina 004.0151
Collana Theoretical Computer Science and General Issues
Soggetto topico Software engineering
Compilers (Computer programs)
Artificial intelligence
Computer science
Computer engineering
Computer networks
Computers
Professions
Software Engineering
Compilers and Interpreters
Artificial Intelligence
Theory of Computation
Computer Engineering and Networks
The Computing Profession
ISBN 3-030-03427-5
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto RV-TheToP: Runtime Verification from the Theory To the industry Practice (Track Introduction) -- Opportunities and Challenges in Monitoring Cyber-physical Systems Security -- Migrating Monitors + ABE: A Suitable Combination for Secure IoT? -- Capturing Inter-Process Communication for Runtime Verification on Android -- Considering Academia-Industry Projects Meta-Characteristics in Runtime Verification Design -- Flexible Monitor Deployment for Runtime Verification of Large Scale Software -- Increasing the Reusability of Enforcers with Lifecycle Events -- BDDs on the Run -- Verifying Real-World Software with Contracts for Concurrency -- Formal Methods in Industrial Practice - bridging the gap (Track Summary) -- Model-based Testing for Avionic Systems -- Proven Benefits and Further Challenges -- Test Case Generation with PathCrawler/LTest: How to Automate an Industrial Testing Process -- Pitfalls in Applying Model Learning to Industrial Legacy Software -- Formal Verification in Automotive Industry: Enablers and Obstacles -- Scalability of Deductive Verification Depends on Method Call Treatment -- Java Automated Deductive Verification in Practice: Lessons from industrial proof-based projects -- Security Filters for IoT Domain Isolation -- 20 Years of Uppaal Enabled Industrial Model-Based Validation and Beyond -- Verification of Operating System Monolithic Kernels without Extensions -- A Proposal of an Example and Experiments Repository to Foster Industrial Adoption of Formal Methods -- Reliable Smart Contracts: State-of-the-art, Applications, Challenges and Future Directions -- Smart Contracts and Opportunities for Formal Methods -- Contracts over Smart Contracts: Recovering from Violations Dynamically -- Security Analysis of Smart Contracts in Datalog -- Temporal Properties of Smart Contracts -- Temporal Aspects of Smart Contracts for Financial Derivatives -- Marlowe: financial contracts on blockchain -- SMT-based Verification of Solidity Smart Contracts -- Blockchains as Kripke Models: an Analysis of Atomic Cross-Chain Swap -- A Language-Independent Approach To Smart Contract Verification -- Towards Adding Variety to Simplicity -- Fun with Bitcoin smart contracts -- Computing Exact Worst-Case Gas Consumption for Smart Contracts -- Digital Transformation Trends: Industry 4.0, Automation, and AI -- A Methodology for Combinatory Process Synthesis: Process Variability in Clinical Pathways -- Automatic composition of rough solution possibilities in the target planning of factory planning projects by means of combinatory logic -- GOLD: Global Organization aLignment and Decision - Towards the Hierarchical Integration of Heterogeneous Business Models.
Record Nr. UNINA-9910349396703321
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Leveraging Applications of Formal Methods, Verification and Validation. Modeling [[electronic resource] ] : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I / / edited by Tiziana Margaria, Bernhard Steffen
Leveraging Applications of Formal Methods, Verification and Validation. Modeling [[electronic resource] ] : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I / / edited by Tiziana Margaria, Bernhard Steffen
Edizione [1st ed. 2018.]
Pubbl/distr/stampa Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Descrizione fisica 1 online resource (XV, 588 p. 229 illus., 136 illus. in color.)
Disciplina 004.0151
Collana Theoretical Computer Science and General Issues
Soggetto topico Software engineering
Compilers (Computer programs)
Artificial intelligence
Computer science
Computer engineering
Computer networks
Computers
Professions
Software Engineering
Compilers and Interpreters
Artificial Intelligence
Theory of Computation
Computer Engineering and Networks
The Computing Profession
ISBN 3-030-03418-6
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Towards a Unified View of Modeling and Programming - ISoLA 2018 Track Introduction -- On Modeling and Programming -- Definition of Modeling vs. Programming Languages -- A Non-unified View of Modelling, Specification and Programming -- Using Umple to Synergistically Process Features, Variants, UML Models and Classic Code -- Why Programming Must Be Supported by Modeling and How -- On Models and Code - A Unified Approach to Support Large-Scale Deductive Program Verification -- Type Theory as a Framework for Modelling and Programming -- Bringing Effortless Refinement of Data Layouts to Cogent -- Programming Is Modeling -- Programming language specification and implementation -- Modeling with Scala -- This is not a model -- A Unified Approach for Modeling, Developing, and Assuring Critical Systems -- Towards Interactive Compilation Models -- From Computational Thinking to Constructive Design with Simple Models -- Design Languages: A Necessary New Generation of Computer Languages -- From Modeling to Model-based Programming -- Fusing Modeling and Programming into Language-Oriented Programming -- On the Difficulty of Drawing the Line -- X-by-Construction - Track Introduction -- (Some) security by construction through a LangSec approach -- Program Correctness by Transformation -- Design 4 X through Model Transformation -- Modelling by Patterns for Correct-by-Construction Process -- Modular, Correct Compilation with Automatic Soundness Proofs -- Deployment by Construction for Multicore Architectures -- Towards Software Performance by Construction -- Is Privacy by Construction Possible? -- X-by-C: Non-Functional Security -- Towards Confidentiality-by-Construction -- A Tutorial Introduction to Graphical Modeling and Metamodeling with CINCO -- Model-based Development for High-Assurance Embedded Systems -- DSLs for Decision Services: A Tutorial Introduction to Language-Driven Engineering -- Tutorial: an Overview of Malware Detection and Evasion Techniques.
Record Nr. UNISA-996466452803316
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Leveraging Applications of Formal Methods, Verification and Validation. Modeling : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I / / edited by Tiziana Margaria, Bernhard Steffen
Leveraging Applications of Formal Methods, Verification and Validation. Modeling : 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part I / / edited by Tiziana Margaria, Bernhard Steffen
Edizione [1st ed. 2018.]
Pubbl/distr/stampa Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Descrizione fisica 1 online resource (XV, 588 p. 229 illus., 136 illus. in color.)
Disciplina 004.0151
Collana Theoretical Computer Science and General Issues
Soggetto topico Software engineering
Compilers (Computer programs)
Artificial intelligence
Computer science
Computer engineering
Computer networks
Computers
Professions
Software Engineering
Compilers and Interpreters
Artificial Intelligence
Theory of Computation
Computer Engineering and Networks
The Computing Profession
ISBN 3-030-03418-6
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Towards a Unified View of Modeling and Programming - ISoLA 2018 Track Introduction -- On Modeling and Programming -- Definition of Modeling vs. Programming Languages -- A Non-unified View of Modelling, Specification and Programming -- Using Umple to Synergistically Process Features, Variants, UML Models and Classic Code -- Why Programming Must Be Supported by Modeling and How -- On Models and Code - A Unified Approach to Support Large-Scale Deductive Program Verification -- Type Theory as a Framework for Modelling and Programming -- Bringing Effortless Refinement of Data Layouts to Cogent -- Programming Is Modeling -- Programming language specification and implementation -- Modeling with Scala -- This is not a model -- A Unified Approach for Modeling, Developing, and Assuring Critical Systems -- Towards Interactive Compilation Models -- From Computational Thinking to Constructive Design with Simple Models -- Design Languages: A Necessary New Generation of Computer Languages -- From Modeling to Model-based Programming -- Fusing Modeling and Programming into Language-Oriented Programming -- On the Difficulty of Drawing the Line -- X-by-Construction - Track Introduction -- (Some) security by construction through a LangSec approach -- Program Correctness by Transformation -- Design 4 X through Model Transformation -- Modelling by Patterns for Correct-by-Construction Process -- Modular, Correct Compilation with Automatic Soundness Proofs -- Deployment by Construction for Multicore Architectures -- Towards Software Performance by Construction -- Is Privacy by Construction Possible? -- X-by-C: Non-Functional Security -- Towards Confidentiality-by-Construction -- A Tutorial Introduction to Graphical Modeling and Metamodeling with CINCO -- Model-based Development for High-Assurance Embedded Systems -- DSLs for Decision Services: A Tutorial Introduction to Language-Driven Engineering -- Tutorial: an Overview of Malware Detection and Evasion Techniques.
Record Nr. UNINA-9910349396603321
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering [[electronic resource] ] : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part II / / edited by Tiziana Margaria, Bernhard Steffen
Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering [[electronic resource] ] : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part II / / edited by Tiziana Margaria, Bernhard Steffen
Edizione [1st ed. 2022.]
Pubbl/distr/stampa Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2022
Descrizione fisica 1 online resource (436 pages)
Disciplina 005.1
Collana Lecture Notes in Computer Science
Soggetto topico Software engineering
Artificial intelligence
Computer science
Computer engineering
Computer networks
Computers, Special purpose
Computer systems
Software Engineering
Artificial Intelligence
Theory of Computation
Computer Engineering and Networks
Special Purpose and Application-Based Systems
Computer System Implementation
ISBN 3-031-19756-9
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Programming - What is Next: The Role of Documentation -- Automated Software Re-Engineering -- DIME Days.
Record Nr. UNISA-996495569103316
Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2022
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part II / / edited by Tiziana Margaria, Bernhard Steffen
Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering : 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part II / / edited by Tiziana Margaria, Bernhard Steffen
Edizione [1st ed. 2022.]
Pubbl/distr/stampa Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2022
Descrizione fisica 1 online resource (436 pages)
Disciplina 005.1
Collana Lecture Notes in Computer Science
Soggetto topico Software engineering
Artificial intelligence
Computer science
Computer engineering
Computer networks
Computers, Special purpose
Computer systems
Software Engineering
Artificial Intelligence
Theory of Computation
Computer Engineering and Networks
Special Purpose and Application-Based Systems
Computer System Implementation
ISBN 3-031-19756-9
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Programming - What is Next: The Role of Documentation -- Automated Software Re-Engineering -- DIME Days.
Record Nr. UNINA-9910619286403321
Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2022
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui