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.
Correct Hardware Design and Verification Methods [[electronic resource] ] : 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001 Livingston, Scotland, UK, September 4-7, 2001 Proceedings / / edited by Tiziana Margaria, Tom Melham
| Correct Hardware Design and Verification Methods [[electronic resource] ] : 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001 Livingston, Scotland, UK, September 4-7, 2001 Proceedings / / edited by Tiziana Margaria, Tom Melham |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XII, 488 p.) |
| Disciplina | 621.39/5 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Architecture, Computer
Computers Software engineering Computer hardware Computer logic Computer System Implementation Theory of Computation Software Engineering/Programming and Operating Systems Computer Hardware Logics and Meanings of Programs Software Engineering |
| ISBN | 3-540-44798-9 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- View from the Fringe of the Fringe -- Hardware Synthesis Using SAFL and Application to Processor Design -- FMCAD 2000 -- Applications of Hierarchical Verification in Model Checking -- Model Checking 1 -- Pruning Techniques for the SAT-Based Bounded Model Checking Problem -- Heuristics for Hierarchical Partitioning with Application to Model Checking -- Short Papers 1 -- Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs -- Deriving Real-Time Programs from Duration Calculus Specifications -- Reproducing Synchronization Bugs with Model Checking -- Formally-Based Design Evaluation -- Clocking Issues -- Multiclock Esterel -- Register Transformations with Multiple Clock Domains -- Temporal Properties of Self-Timed Rings -- Short Papers 2 -- Coverability Analysis Using Symbolic Model Checking -- Specifying Hardware Timing with ET-Lotos -- Formal Pipeline Design -- Verification of Basic Block Schedules Using RTL Transformations -- Joint Session with TPHOLs -- Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking -- Proof Engineering in the Large: Formal Verification of Pentium®4 Floating-Point Divider -- Hardware Compilation -- Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques -- A Higher-Level Language for Hardware Synthesis -- Tools -- Hierarchical Verification Using an MDG-HOL Hybrid Tool -- Exploiting Transition Locality in Automatic Verification -- Efficient Debugging in a Formal Verification Environment -- Model Checking 2 -- Using Combinatorial Optimization Methods for Quantification Scheduling -- Net Reductions for LTL Model-Checking -- Component Verification -- Formal Verification of the VAMP Floating Point Unit -- A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® Itanium™ Processor Bus Protocol -- The Design and Verification of a Sorter Core -- Case Studies -- Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip -- Using Abstract Specifications to Verify PowerPC™ Custom Memories by Symbolic Trajectory Evaluation -- Algorithm Verification -- Formal Verification of Conflict Detection Algorithms -- Induction-Oriented Formal Verification in Symmetric Interconnection Networks -- A Framework for Microprocessor Correctness Statements -- Duration Calculus -- From Operational Semantics to Denotational Semantics for Verilog -- Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming. |
| Record Nr. | UNINA-9910143627203321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Correct Hardware Design and Verification Methods [[electronic resource] ] : 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001 Livingston, Scotland, UK, September 4-7, 2001 Proceedings / / edited by Tiziana Margaria, Tom Melham
| Correct Hardware Design and Verification Methods [[electronic resource] ] : 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001 Livingston, Scotland, UK, September 4-7, 2001 Proceedings / / edited by Tiziana Margaria, Tom Melham |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XII, 488 p.) |
| Disciplina | 621.39/5 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Architecture, Computer
Computers Software engineering Computer hardware Computer logic Computer System Implementation Theory of Computation Software Engineering/Programming and Operating Systems Computer Hardware Logics and Meanings of Programs Software Engineering |
| ISBN | 3-540-44798-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- View from the Fringe of the Fringe -- Hardware Synthesis Using SAFL and Application to Processor Design -- FMCAD 2000 -- Applications of Hierarchical Verification in Model Checking -- Model Checking 1 -- Pruning Techniques for the SAT-Based Bounded Model Checking Problem -- Heuristics for Hierarchical Partitioning with Application to Model Checking -- Short Papers 1 -- Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs -- Deriving Real-Time Programs from Duration Calculus Specifications -- Reproducing Synchronization Bugs with Model Checking -- Formally-Based Design Evaluation -- Clocking Issues -- Multiclock Esterel -- Register Transformations with Multiple Clock Domains -- Temporal Properties of Self-Timed Rings -- Short Papers 2 -- Coverability Analysis Using Symbolic Model Checking -- Specifying Hardware Timing with ET-Lotos -- Formal Pipeline Design -- Verification of Basic Block Schedules Using RTL Transformations -- Joint Session with TPHOLs -- Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking -- Proof Engineering in the Large: Formal Verification of Pentium®4 Floating-Point Divider -- Hardware Compilation -- Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques -- A Higher-Level Language for Hardware Synthesis -- Tools -- Hierarchical Verification Using an MDG-HOL Hybrid Tool -- Exploiting Transition Locality in Automatic Verification -- Efficient Debugging in a Formal Verification Environment -- Model Checking 2 -- Using Combinatorial Optimization Methods for Quantification Scheduling -- Net Reductions for LTL Model-Checking -- Component Verification -- Formal Verification of the VAMP Floating Point Unit -- A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® Itanium™ Processor Bus Protocol -- The Design and Verification of a Sorter Core -- Case Studies -- Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip -- Using Abstract Specifications to Verify PowerPC™ Custom Memories by Symbolic Trajectory Evaluation -- Algorithm Verification -- Formal Verification of Conflict Detection Algorithms -- Induction-Oriented Formal Verification in Symmetric Interconnection Networks -- A Framework for Microprocessor Correctness Statements -- Duration Calculus -- From Operational Semantics to Denotational Semantics for Verilog -- Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming. |
| Record Nr. | UNISA-996465808803316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Engineering of Computer-Based Systems : 8th International Conference, ECBS 2023, Västerås, Sweden, October 16-18, 2023, Proceedings / / Jan Kofron, Tiziana Margaria, and Cristina Seceleanu, editors
| Engineering of Computer-Based Systems : 8th International Conference, ECBS 2023, Västerås, Sweden, October 16-18, 2023, Proceedings / / Jan Kofron, Tiziana Margaria, and Cristina Seceleanu, editors |
| Edizione | [First edition.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer Nature Switzerland AG, , [2024] |
| Descrizione fisica | 1 online resource (312 pages) |
| Disciplina | 621.39 |
| Collana | Lecture Notes in Computer Science Series |
| Soggetto topico |
Computer engineering
Systems engineering |
| ISBN | 3-031-49252-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | How To Be An Ethical Technologist -- Toward Responsible Artificial Intelligence systems -- Safety and trustworthiness -- Ambient Temperature Prediction for Embedded Systems using Machine Learning -- A Federated Learning Algorithms Development Paradigm -- Machine Learning Data Suitability and Performance Testing Using Fault Injection Testing Framework -- Samuelsson IDPP: Imbalanced Datasets Pipelines in Pyrus -- Learning in Uppaal for Test Case Generation for Cyber-Physical Systems -- A Literature Survey of Assertions in Software Testing -- FPGA-based encryption for peer-to-peer industrial network links -- Formalization and Verification of MQTT-SN Communication Using CSP -- Environments using Acoustic Classification for Sensor Fusion with Radar systems -- Comparative Analysis of UPPAAL SMC, ns-3 and MATLAB/Simulink -- Using Automata Learning for Compliance Evaluation of Communcation Protocols on an NFC Handshake Example -- Towards LLM-based System Migration in Language-Driven Engineering -- Synthesizing Understandable Strategies -- ReProInspect: Framework for Reproducible Defect Datasets for Improved AOI of PCBAs -- Cyber-Physical Ecosystems: Modelling and Verification -- Integrating IoT Infrastructures in Industrie 4.0 Scenarios with the Asset Administration Shell -- A Software Package (in progress) that implements the Dynamic Priority Scheduling for Periodic Systems using ROS 2 -- Continuous Integration of Neural Networks in Autonomous Systems -- Building a Digital Twin Framework for Dynamic and Robust Distributed Systems -- A simple end-to-end computer-aided detection pipeline for trained deep learning models. Case pipeline: Pulmonary embolism detection -- Astrocyte-Integrated Dynamic Function Exchange in Spiking Neural Networks -- Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP -- Combining Machine Learning and Virtual Reality to Build an Attractive Job Recommender System for Youth: Technical Details and Experimental Data. |
| Record Nr. | UNINA-9910766890203321 |
| Cham, Switzerland : , : Springer Nature Switzerland AG, , [2024] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Engineering of Computer-Based Systems : 8th International Conference, ECBS 2023, Västerås, Sweden, October 16-18, 2023, Proceedings / / Jan Kofron, Tiziana Margaria, and Cristina Seceleanu, editors
| Engineering of Computer-Based Systems : 8th International Conference, ECBS 2023, Västerås, Sweden, October 16-18, 2023, Proceedings / / Jan Kofron, Tiziana Margaria, and Cristina Seceleanu, editors |
| Edizione | [First edition.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer Nature Switzerland AG, , [2024] |
| Descrizione fisica | 1 online resource (312 pages) |
| Disciplina | 621.39 |
| Collana | Lecture Notes in Computer Science Series |
| Soggetto topico |
Computer engineering
Systems engineering |
| ISBN | 3-031-49252-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | How To Be An Ethical Technologist -- Toward Responsible Artificial Intelligence systems -- Safety and trustworthiness -- Ambient Temperature Prediction for Embedded Systems using Machine Learning -- A Federated Learning Algorithms Development Paradigm -- Machine Learning Data Suitability and Performance Testing Using Fault Injection Testing Framework -- Samuelsson IDPP: Imbalanced Datasets Pipelines in Pyrus -- Learning in Uppaal for Test Case Generation for Cyber-Physical Systems -- A Literature Survey of Assertions in Software Testing -- FPGA-based encryption for peer-to-peer industrial network links -- Formalization and Verification of MQTT-SN Communication Using CSP -- Environments using Acoustic Classification for Sensor Fusion with Radar systems -- Comparative Analysis of UPPAAL SMC, ns-3 and MATLAB/Simulink -- Using Automata Learning for Compliance Evaluation of Communcation Protocols on an NFC Handshake Example -- Towards LLM-based System Migration in Language-Driven Engineering -- Synthesizing Understandable Strategies -- ReProInspect: Framework for Reproducible Defect Datasets for Improved AOI of PCBAs -- Cyber-Physical Ecosystems: Modelling and Verification -- Integrating IoT Infrastructures in Industrie 4.0 Scenarios with the Asset Administration Shell -- A Software Package (in progress) that implements the Dynamic Priority Scheduling for Periodic Systems using ROS 2 -- Continuous Integration of Neural Networks in Autonomous Systems -- Building a Digital Twin Framework for Dynamic and Robust Distributed Systems -- A simple end-to-end computer-aided detection pipeline for trained deep learning models. Case pipeline: Pulmonary embolism detection -- Astrocyte-Integrated Dynamic Function Exchange in Spiking Neural Networks -- Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP -- Combining Machine Learning and Virtual Reality to Build an Attractive Job Recommender System for Youth: Technical Details and Experimental Data. |
| Record Nr. | UNISA-996565865103316 |
| Cham, Switzerland : , : Springer Nature Switzerland AG, , [2024] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Leveraging Applications of Formal Methods, Verification and Validation [[electronic resource] ] : 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Rhodes, Greece, October 17–29, 2021, Proceedings / / edited by Tiziana Margaria, Bernhard Steffen
| Leveraging Applications of Formal Methods, Verification and Validation [[electronic resource] ] : 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Rhodes, Greece, October 17–29, 2021, Proceedings / / edited by Tiziana Margaria, Bernhard Steffen |
| Edizione | [1st ed. 2021.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
| Descrizione fisica | 1 online resource (505 pages) |
| Disciplina | 006.3 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Artificial intelligence Computer programming Compilers (Computer programs) Application software Software Engineering Artificial Intelligence Programming Techniques Compilers and Interpreters Computer and Information Systems Applications |
| ISBN | 3-030-89159-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | STRESS - Introduction -- An Introduction to Graphical Modeling of CI/CD Workflows with Rig -- Pyrus: an Online Modeling Environment for No-Code Data-Analytics Service Composition -- Integrating External Services in DIME -- Asking Why -- Formal Methods for a Digital Industry: Industrial Day at ISoLA 2021 -- Agile Business Engineering: From Transformation Towards Continuous Innovation -- Towards Living Canvases -- Use Cases for Simulation in the Development of Automated Driving Systems -- Simulation-based Elicitation of Accuracy Requirements for the Environmental Perception of Autonomous Vehicles -- DSLs and Middleware Platforms in a Model-Driven Development Approach for Secure Predictive Maintenance Systems in Smart Factories -- From Requirements to Executable Rules: An Ensemble of Domain-Specific Languages for Programming Cyber-Physical Systems in Warehouse Logistics -- Mining Data Quality Rules for Data Migrations: A Case Study on Material Master Data -- Programming - What is Next? -- Low-Code is Often High-Code, So We Must Design Low-Code Platforms to Enable Proper Software Engineering -- Time for All Programs, Not Just Real-Time Programs -- Integrated Modeling and Development of Component-Based Embedded Software in Scala -- Slang: The Sireum Programming Language -- HAMR: An AADL Multi-Platform Code Generation Toolset -- Fundamental Constructs in Programming Languages -- Introducing Dynamical Systems and Chaos Early in Computer Science and Software Engineering Education can Help Advance Theory and Practice of Software Development and Computing -- GATE: Gradual Effect Types -- Fixing Classification: A Viewpoint-based Approach -- The Future of Programming and Modelling: a Vision -- Towards Model-based Intent-Driven Adaptive Software -- The Interoperability Challenge: Building a model driven Digital Thread platform for CPS -- Programming vs. That Thing Subject Matter Experts Do -- Aligned, Purpose-Driven Cooperation: The Future Way of System Development -- RAILS: Roadmaps for AI integration in the raiL Sector -- A Journey through Software Model Checking of Interlocking Programs -- Supporting the Development of Hybrid ERTMS/ETCS Level 3 with Formal Modelling, Analysis and Simulation -- Formal Methods in Railway Signalling Infrastructure Standardisation Processes -- sVerify: Verifying Smart Contracts through Lazy Annotation and Learning -- Verifying temporal properties of stigmergic collective systems using CADP. |
| Record Nr. | UNINA-9910502669603321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Leveraging Applications of Formal Methods, Verification and Validation [[electronic resource] ] : 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Rhodes, Greece, October 17–29, 2021, Proceedings / / edited by Tiziana Margaria, Bernhard Steffen
| Leveraging Applications of Formal Methods, Verification and Validation [[electronic resource] ] : 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Rhodes, Greece, October 17–29, 2021, Proceedings / / edited by Tiziana Margaria, Bernhard Steffen |
| Edizione | [1st ed. 2021.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
| Descrizione fisica | 1 online resource (505 pages) |
| Disciplina | 006.3 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Artificial intelligence Computer programming Compilers (Computer programs) Application software Software Engineering Artificial Intelligence Programming Techniques Compilers and Interpreters Computer and Information Systems Applications |
| ISBN | 3-030-89159-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | STRESS - Introduction -- An Introduction to Graphical Modeling of CI/CD Workflows with Rig -- Pyrus: an Online Modeling Environment for No-Code Data-Analytics Service Composition -- Integrating External Services in DIME -- Asking Why -- Formal Methods for a Digital Industry: Industrial Day at ISoLA 2021 -- Agile Business Engineering: From Transformation Towards Continuous Innovation -- Towards Living Canvases -- Use Cases for Simulation in the Development of Automated Driving Systems -- Simulation-based Elicitation of Accuracy Requirements for the Environmental Perception of Autonomous Vehicles -- DSLs and Middleware Platforms in a Model-Driven Development Approach for Secure Predictive Maintenance Systems in Smart Factories -- From Requirements to Executable Rules: An Ensemble of Domain-Specific Languages for Programming Cyber-Physical Systems in Warehouse Logistics -- Mining Data Quality Rules for Data Migrations: A Case Study on Material Master Data -- Programming - What is Next? -- Low-Code is Often High-Code, So We Must Design Low-Code Platforms to Enable Proper Software Engineering -- Time for All Programs, Not Just Real-Time Programs -- Integrated Modeling and Development of Component-Based Embedded Software in Scala -- Slang: The Sireum Programming Language -- HAMR: An AADL Multi-Platform Code Generation Toolset -- Fundamental Constructs in Programming Languages -- Introducing Dynamical Systems and Chaos Early in Computer Science and Software Engineering Education can Help Advance Theory and Practice of Software Development and Computing -- GATE: Gradual Effect Types -- Fixing Classification: A Viewpoint-based Approach -- The Future of Programming and Modelling: a Vision -- Towards Model-based Intent-Driven Adaptive Software -- The Interoperability Challenge: Building a model driven Digital Thread platform for CPS -- Programming vs. That Thing Subject Matter Experts Do -- Aligned, Purpose-Driven Cooperation: The Future Way of System Development -- RAILS: Roadmaps for AI integration in the raiL Sector -- A Journey through Software Model Checking of Interlocking Programs -- Supporting the Development of Hybrid ERTMS/ETCS Level 3 with Formal Modelling, Analysis and Simulation -- Formal Methods in Railway Signalling Infrastructure Standardisation Processes -- sVerify: Verifying Smart Contracts through Lazy Annotation and Learning -- Verifying temporal properties of stigmergic collective systems using CADP. |
| Record Nr. | UNISA-996464522603316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Leveraging Applications of Formal Methods, Verification and Validation [[electronic resource] ] : 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part I / / edited by Tiziana Margaria, Bernhard Steffen
| Leveraging Applications of Formal Methods, Verification and Validation [[electronic resource] ] : 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part I / / edited by Tiziana Margaria, Bernhard Steffen |
| Edizione | [1st ed. 2012.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
| Descrizione fisica | 1 online resource (XVI, 617 p. 170 illus.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Operating systems (Computers) Computer science Artificial intelligence Software Engineering Compilers and Interpreters Operating Systems Theory of Computation Computer Science Logic and Foundations of Programming Artificial Intelligence |
| ISBN | 3-642-34026-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Adaptable and Evolving Software for Eternal Systems (Track Summary).- Challenges in Defining a Programming Language for Provably Correct Dynamic Analyses.- Eternal Embedded Software: Towards Innovation Experiment Systems.- A Liskov Principle for Delta-Oriented Programming -- Scientific Workflows: Eternal Components, Changing Interfaces, Varying Compositions.- An Object Group-Based Component Model.- Automated Inference of Models for Black Box Systems Based on Interface Descriptions.- Model-Based Compatibility Checking of System Modifications.- A Generic Platform for Model-Based Regression Testing.- Approaches for Mastering Change.- A Formal Approach to Software Product Families.- A Compositional Framework to Derive Product Line Behavioural Descriptions.- Delta-Oriented Monitor Specification.- Conflict Detection in Delta-Oriented Programming.- Family-Based Analysis of Type Safety for Delta-Oriented Software Product Lines.- A Vision for Behavioural Model-Driven Validation of Software Product Lines.- Parameterized Preorder Relations for Model-Based Testing of Software Product Lines.- SmartTies – Management of Safety-Critical Developments.- Tracking Behavioral Constraints during Object-Oriented Software Evolution.- Towards the Verification of Adaptable Processes.- Runtime Verification: The Application Perspective.- What Does AI Have to Do with RV? (Extended Abstract).- A Case for “Piggyback” Runtime Monitoring.- A Unified Approach for Static and Runtime Verification: Framework and Applications.- Statistical Model Checking QoS Properties of Systems with SBIP.- Monitoring Temporal Information Flow.- Dynamic Information-Flow Analysis for Multi-threaded Applications.- Bounded-Interference Sequentialization for Testing Concurrent Programs.- Runtime Verification of Biological Systems.- Behavioral Specification Based Runtime Monitors for OSGi Services.- Modelling and Decentralised Runtime Control of Self-stabilising Power Micro Grids.- Model-Based Testing and Model Inference.- Algorithmic Improvements on Regular Inference of Software Models and Perspectives for Security Testing.- Test-Case Design by Feature Trees.- Model-Based Static Code Analysis for MATLAB Models.- An Incremental Learning Algorithm for Extended Mealy Automata.- Learning Techniques for Software Verification and Validation.- Learning Stochastic Timed Automata from Sample Executions.- Learning Minimal Deterministic Automata from Inexperienced Teachers.- Model Learning and Test Generation for Event-B Decomposition.- Inferring Semantic Interfaces of Data Structures.- Learning-Based Test Programming for Programmers.- LearnLib Tutorial: From Finite Automata to Register Interface Programs.- Automated Learning Setups in Automata Learning.- The RERS Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems. Challenges in Defining a Programming Language for Provably Correct Dynamic Analyses.- Eternal Embedded Software: Towards Innovation Experiment Systems.- A Liskov Principle for Delta-Oriented Programming -- Scientific Workflows: Eternal Components, Changing Interfaces, Varying Compositions.- An Object Group-Based Component Model.- Automated Inference of Models for Black Box Systems Based on Interface Descriptions.- Model-Based Compatibility Checking of System Modifications.- A Generic Platform for Model-Based Regression Testing.- Approaches for Mastering Change.- A Formal Approach to Software Product Families.- A Compositional Framework to Derive Product Line Behavioural Descriptions.- Delta-Oriented Monitor Specification.- Conflict Detection in Delta-Oriented Programming.- Family-Based Analysis of Type Safety for Delta-Oriented Software Product Lines.- A Vision for Behavioural Model-Driven Validation of Software Product Lines.- Parameterized Preorder Relations for Model-Based Testing of Software Product Lines.- SmartTies – Management of Safety-Critical Developments.- Tracking Behavioral Constraints during Object-Oriented Software Evolution.- Towards the Verification of Adaptable Processes.- Runtime Verification: The Application Perspective.- What Does AI Have to Do with RV? (Extended Abstract).- A Case for “Piggyback” Runtime Monitoring.- A Unified Approach for Static and Runtime Verification: Framework and Applications.- Statistical Model Checking QoS Properties of Systems with SBIP.- Monitoring Temporal Information Flow.- Dynamic Information-Flow Analysis for Multi-threaded Applications.- Bounded-Interference Sequentialization for Testing Concurrent Programs.- Runtime Verification of Biological Systems.- Behavioral Specification Based Runtime Monitors for OSGi Services.- Modelling and Decentralised Runtime Control of Self-stabilising Power Micro Grids.- Model-Based Testing and Model Inference.- Algorithmic Improvements on Regular Inference of Software Models and Perspectives for Security Testing.- Test-Case Design by Feature Trees.- Model-Based Static Code Analysis for MATLAB Models.- An Incremental Learning Algorithm for Extended Mealy Automata.- Learning Techniques for Software Verification and Validation.- Learning Stochastic Timed Automata from Sample Executions.- Learning Minimal Deterministic Automata from Inexperienced Teachers.- Model Learning and Test Generation for Event-B Decomposition.- Inferring Semantic Interfaces of Data Structures.- Learning-Based Test Programming for Programmers.- LearnLib Tutorial: From Finite Automata to Register Interface Programs.- Automated Learning Setups in Automata Learning.- The RERS Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems. |
| Record Nr. | UNISA-996466193003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Leveraging Applications of Formal Methods, Verification and Validation [[electronic resource] ] : 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part II / / edited by Tiziana Margaria, Bernhard Steffen
| Leveraging Applications of Formal Methods, Verification and Validation [[electronic resource] ] : 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15-18, 2012, Proceedings, Part II / / edited by Tiziana Margaria, Bernhard Steffen |
| Edizione | [1st ed. 2012.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
| Descrizione fisica | 1 online resource (XVI, 361 p. 129 illus.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Operating systems (Computers) Computer science Artificial intelligence Software Engineering Compilers and Interpreters Operating Systems Theory of Computation Computer Science Logic and Foundations of Programming Artificial Intelligence |
| ISBN | 3-642-34032-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Linux Driver Verification (Position Paper).- Bioscientific Data Processing and Modeling.- Using Multiobjective Optimization and Energy Minimization to Design an Isoform-Selective Ligand of the 14-3-3 Protein.- Segmentation for High-Throughput Image Analysis: Watershed Masked Clustering.- Efficient and Robust Shape Retrieval from Deformable Templates.- OWL-DL Domain-Models as Abstract Workflows.- Processes and Data Integration in the Networked Healthcare.- Simple Modeling of Executable Role-Based Workflows: An Application in the Healthcare Domain.- Considerations for Healthcare Applications in a Platform as a Service Environment.- Reha-Sports: The Challenge of Small Margin Healthcare Accounting.- Timing Constraints: Theory Meets Practice.- A Simple and Flexible Timing Constraint Logic.- Generalized Weakly-Hard Constraints.- Modeling a BSG-E Automotive System with the Timing Augmented Description Language.- Formal Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method.- Formal Specification and Verification of Task Time Constraints for Real-Time Systems.- The WCET Analysis Tool CalcWcet167.- Abstract Execution for Event-Driven Systems – An Application from Automotive/Infotainment Development.- Formal Methods for Intelligent Transportation Systems.- Model-Driven V&V Processes for Computer Based Control Systems: A Unifying Perspective.- Formal Methods in Avionic Software Certification: The DO-178C Perspective.- Product Line Engineering Applied to CBTC Systems Development.- Improving Verification Process in Driverless Metro Systems: The MBAT Project.- Optimising Ordering Strategies for Symbolic Model Checking of Railway Interlockings.- Automated Generation of Safety Requirements from Railway Interlocking Tables.- Distributing the Challenge of Model Checking Interlocking Control Tables.- Quantitative Modelling and Analysis.- Schedulability of Herschel-Planck Revisited Using Statistical Model Checking.- Checking Correctness of Services Modeled as Priced Timed Automata.- Software Aspects of Robotic Systems.- Process-Oriented Geoinformation Systems and Applications.- Concepts and Techniques of an Online 3D Atlas – Challenges in Cartographic 3D Geovisualization.- Handling Heterogeneity in Formal Developments of Hardware and Software Systems -- Formal Verification Tools for DSML Users: A Process Modeling Case Study.- An Ontological Pivot Model to Interoperate Heterogeneous User Requirements. Bioscientific Data Processing and Modeling.- Using Multiobjective Optimization and Energy Minimization to Design an Isoform-Selective Ligand of the 14-3-3 Protein.- Segmentation for High-Throughput Image Analysis: Watershed Masked Clustering.- Efficient and Robust Shape Retrieval from Deformable Templates.- OWL-DL Domain-Models as Abstract Workflows.- Processes and Data Integration in the Networked Healthcare.- Simple Modeling of Executable Role-Based Workflows: An Application in the Healthcare Domain.- Considerations for Healthcare Applications in a Platform as a Service Environment.- Reha-Sports: The Challenge of Small Margin Healthcare Accounting.- Timing Constraints: Theory Meets Practice.- A Simple and Flexible Timing Constraint Logic.- Generalized Weakly-Hard Constraints.- Modeling a BSG-E Automotive System with the Timing Augmented Description Language.- Formal Analysis of TESLA Protocol in the Timed OTS/CafeOBJ Method.- Formal Specification and Verification of Task Time Constraints for Real-Time Systems.- The WCET Analysis Tool CalcWcet167.- Abstract Execution for Event-Driven Systems – An Application from Automotive/Infotainment Development.- Formal Methods for Intelligent Transportation Systems.- Model-Driven V&V Processes for Computer Based Control Systems: A Unifying Perspective.- Formal Methods in Avionic Software Certification: The DO-178C Perspective.- Product Line Engineering Applied to CBTC Systems Development.- Improving Verification Process in Driverless Metro Systems: The MBAT Project.- Optimising Ordering Strategies for Symbolic Model Checking of Railway Interlockings.- Automated Generation of Safety Requirements from Railway Interlocking Tables.- Distributing the Challenge of Model Checking Interlocking Control Tables.- Quantitative Modelling and Analysis.- Schedulability of Herschel-Planck Revisited Using Statistical Model Checking.- Checking Correctness of Services Modeled as Priced Timed Automata.- Software Aspects of Robotic Systems.- Process-Oriented Geoinformation Systems and Applications.- Concepts and Techniques of an Online 3D Atlas – Challenges in Cartographic 3D Geovisualization.- Handling Heterogeneity in Formal Developments of Hardware and Software Systems -- Formal Verification Tools for DSML Users: A Process Modeling Case Study.- An Ontological Pivot Model to Interoperate Heterogeneous User Requirements. |
| Record Nr. | UNISA-996466210503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Leveraging applications of formal methods, verification and validation, adaptation and learning. Practice : 11th international symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings, Part IV / / Tiziana Margaria-Steffen, Bernhard Steffen, editors
| Leveraging applications of formal methods, verification and validation, adaptation and learning. Practice : 11th international symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings, Part IV / / Tiziana Margaria-Steffen, Bernhard Steffen, editors |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (431 pages) |
| Disciplina | 005.14 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer software - Verification
Formal methods (Computer science) |
| ISBN | 3-031-19762-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Introduction -- Organization -- Contents - Part IV -- Digital Twin Engineering -- Engineering of Digital Twins for Cyber-Physical Systems -- 1 Introduction -- 2 Contributions -- 3 Concluding Remarks -- References -- Towards Requirements Engineering for Digital Twins of Cyber-Physical Systems -- 1 Introduction -- 2 Context -- 3 Requirements Engineering for Digital Twins -- 3.1 Requirements Elicitation -- 3.2 Requirements Specification and Modeling -- 3.3 Requirements Verification and Validation -- 4 Common DT Requirements -- 4.1 Data Synchronization Between DT and CPS -- 4.2 Modeling Paradigms and Model Fidelity of DT Models -- 4.3 Extra-functional Requirements -- 4.4 DT Evolution -- 4.5 RE for Dealing with Uncertainty -- 4.6 Requirements Engineering for AI for DT -- 4.7 AI for RE for DT -- 5 State of the Art -- 6 Conclusion -- References -- Digital Twins for Organ Preservation Devices -- 1 Introduction -- 2 Digital Twins -- 2.1 Aims and Benefits -- 2.2 Challenges -- 2.3 Medical Applications -- 3 Medical Devices -- 3.1 Challenges -- 3.2 Organ Preservation -- 4 Case Study: ScubaTx™ Organ Preservation Device -- 4.1 The Device -- 4.2 The Software -- 4.3 Challenges -- 5 Discussion -- 5.1 Beyond Organ Preservation -- References -- Using Digital Twins in the Development of Complex Dependable Real-Time Embedded Systems -- 1 Introduction -- 2 The DTiL-RTES Framework -- 2.1 Design Philosophy -- 2.2 DTiL-RTES Overview and Components -- 2.3 Intended Use and Overhead -- 3 ETM Modelling and Refinement -- 3.1 Execution Time Model -- 3.2 Offline Profiling of CRP Model -- 3.3 Prediction Error -- 3.4 Continuous Refinement Through Naive Feedback -- 3.5 Model Refinement Through Condition-Based Model Rebuilding -- 4 Evaluation -- 4.1 Evaluation Setup -- 4.2 Modelling and Residual Error Evaluation.
4.3 Evaluation of Model Refinement and Performance Improvement -- 4.4 Discussion on Safety Challenges -- 5 Related Work -- 5.1 Timing Prediction for Multi-core Real-Time Embedded Systems -- 5.2 Execution Time Modelling -- 6 Conclusion -- References -- Towards Reactive Planning with Digital Twins and Model-Driven Optimization -- 1 Introduction -- 2 Background and Running Example -- 2.1 Automated Planning and Model-Driven Optimization -- 2.2 Digital Twins -- 3 Reactive Planning Framework -- 3.1 Reactive Planning Architecture -- 3.2 Reactive Planning Strategies -- 3.3 Prototypical Implementation -- 3.4 Demonstration Using the Stack Example -- 4 Evaluation -- 4.1 Case Study Setup -- 4.2 Case Study Results -- 4.3 Discussion -- 4.4 Threats to Validity -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Digital Twin Reconfiguration Using Asset Models -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries -- 3.1 Knowledge Bases -- 3.2 Asset Modelling -- 3.3 Simulation Units -- 4 Semantically Lifted Co-simulation -- 5 Structural Reconfiguration in SMOL -- 6 Conclusion -- References -- Formally Verified Self-adaptation of an Incubator Digital Twin -- 1 Introduction -- 2 Background -- 2.1 Notation -- 2.2 Incubator -- 2.3 Flow* Verified Integration -- 2.4 Verified Monitoring -- 3 Formally Verified Self-Adaptation -- 3.1 Incubator Self-Adaptation Loop -- 3.2 Verified Monitoring Architecture for Safe Self-Adaptation -- 3.3 Uncertainty Calibration -- 3.4 Self-adaptation Monitoring and Enforcement -- 4 Incubator Self-adaptation Verification Results -- 4.1 System Setup -- 4.2 Safety Properties -- 4.3 Self-adaptation Results -- 4.4 Repairing the Loop -- 5 Conclusion -- References -- Adaptive Data-driven Predictor of Ship Maneuvering Motion Under Varying Ocean Environments -- 1 Introduction -- 2 Related Work -- 2.1 Incremental Learning. 2.2 Transfer Learning -- 3 Methodology -- 3.1 Gaussian Process Regression -- 3.2 Predictive Anomaly Detection -- 4 Experiment Results -- 4.1 Experiment Setup -- 4.2 Results Analysis -- 5 Conclusion -- References -- Robust Adaptive Back-Stepping Control Approach Using Quadratic Lyapunov Functions for MMC-Based HVDC Digital Twins -- 1 Introduction -- 2 System Description of MMC -- 3 Modeling of the Proposed Adaptive Backstepping Control -- 3.1 Output Current Control -- 3.2 Other Controlling Loops -- 4 Studied HVDC Digital Twin -- 5 Effectiveness of the Proposed Control Method -- 6 Conclusion -- References -- Data-Driven Reachability Analysis of Digital Twin FMI Models -- 1 Introduction -- 2 Preliminaries and Problem Statement -- 2.1 Reachability Analysis and JuliaReach -- 2.2 Co-simulation and Functional Mock-Up Interface -- 2.3 Problem Statement -- 3 Robust Convex Programs -- 4 Simulation-Based Reachability Algorithm -- 4.1 Reachable Set Computation -- 4.2 Lipschitz Constant Estimation via Extreme Value Theorem -- 4.3 Extension to Other Modelling Formalisms -- 5 Validation Exercises -- 5.1 Sampling-Based Lipschitz Constant Estimation -- 5.2 Reachable Set Computation for Linear Systems -- 5.3 Reachable Set Computation for a Nonlinear System -- 6 Conclusions and Future Work -- References -- Towards Secure Digital Twins -- 1 Introduction -- 2 Related Work -- 3 Security Challenges -- 3.1 Bandwidth Sniffing -- 3.2 Data Injection -- 3.3 Data Delay -- 3.4 Model Corruption -- 4 Mitigations -- 4.1 Fragmentation and Data Padding -- 4.2 Signatures and Tokens -- 4.3 Threshold Monitoring and Network-Aware Digital Twin Models -- 4.4 Model Integrity Checks -- 5 Case Study -- 5.1 Physical Twin -- 5.2 Digital Twin -- 5.3 Example Security Challenges -- 6 Open Problems -- 7 Concluding Remarks -- References -- Digital Thread in Smart Manufacturing. Digital Thread in Smart Manufacturing -- 1 Motivation and Goals -- 2 Overview of Contributions -- References -- Integrating Wearable and Camera Based Monitoring in the Digital Twin for Safety Assessment in the Industry 4.0 Era -- 1 Introduction -- 2 Related Work -- 3 Architecture Overview -- 3.1 Wearable Node -- 3.2 HPE Subsystem -- 4 Application Scenario -- 5 Conclusions -- References -- Model-Driven Engineering in Digital Thread Platforms: A Practical Use Case and Future Challenges -- 1 Introduction -- 2 Industrial Use-Case: Safe Operation of Machines -- 2.1 Architecture of the Use Case -- 2.2 The IT Ecosystem: Tools and Technologies -- 3 Access Control Using Attribute Based Encryption -- 3.1 Bilinear Map -- 3.2 Decision Tree -- 3.3 Our Construction -- 4 Conclusions and Reflections -- References -- Trust and Security Analyzer for Collaborative Digital Manufacturing Ecosystems -- 1 Introduction -- 2 Related Work -- 3 Architecture of Digital Thread Connector -- 4 Initial Implementation -- 5 Conclusion -- References -- DISTiL: DIStributed Industrial Computing Environment for Trustworthy DigiTaL Workflows: A Design Perspective -- 1 Introduction -- 1.1 Motivation -- 1.2 Impact for Smart Manufacturing -- 2 DISTiL Design Requirements and Features -- 3 Architecture Design -- 3.1 Distributed Data Layer -- 3.2 Trust-Overlay -- 3.3 Resource Orchestration andProvisioning -- 3.4 Use Case Scenario: Collaborative Predictive Maintenance -- 4 Discussion and Next Steps -- References -- Using Model Selection and Reduction to Develop an Empirical Model to Predict Energy Consumption of a CNC Machine -- 1 Introduction -- 2 Literature Review -- 3 Methodology -- 4 Case Study -- 5 Model Development -- 5.1 Data Preparation -- 5.2 Data Analysis -- 5.3 Data Modelling -- 6 Discussion -- References. Crazy Nodes: Towards Ultimate Flexibility in Ubiquitous Big Data Stream Engineering, Visualisation, and Analytics, in Smart Factories -- 1 Introduction -- 1.1 Reconfigurable Manufacturing -- 1.2 Framework Overview -- 1.3 Paper Structure -- 2 Service and Crazy Nodes -- 2.1 Crazy Nodes -- 2.2 Towards the Cloud -- 3 Proof of Concept -- 4 Conclusions -- References -- Formal Methods for DIStributed COmputing in Future RAILway Systems -- Formal Methods for Distributed Control Systems of Future Railways -- 1 Motivations and Goals -- 2 Contributions -- References -- Safe and Secure Future AI-Driven Railway Technologies: Challenges for Formal Methods in Railway -- 1 Introduction -- 2 Certified Verification of Railway Designs -- 2.1 Automated Verification -- 2.2 Trustworthy and Certifiable Verification -- 2.3 Explainable Verification -- 2.4 Standardisation -- 3 Formal Modelling and Analysis for the Railway Domain -- 3.1 Domain Specific Technology and Usability -- 3.2 Standardised Reference Architectures -- 3.3 Digital Railway Innovations -- 4 Formal Methods for AI -- 4.1 Guaranteeing Safety Behaviour -- 4.2 Learning Formal Models of Railway Behaviour -- 4.3 AI for Monitoring and Maintenance -- 4.4 AI for Optimisation in Scheduling and Design -- 5 Conclusion and Further Work -- References -- Future Train Control Systems: Challenges for Dependability Assessment -- 1 Introduction -- 2 Context -- 2.1 Future Railway Systems -- 2.2 Uncertainty -- 2.3 Dependability Attributes -- 3 Model-Based Evaluation of Dependability -- 3.1 Proposed Modelling Frameworks -- 4 Survey of Railway Case Studies -- 4.1 Performability Evaluation of the ERTMS/ETCS - Level 3 -- 4.2 Safety Evaluation of Moving Block Systems by Statistical Model Checking -- 4.3 Train-to-Train Communication Modeling -- 4.4 Modelling Uncertainty in Satellite Localisation. 4.5 Safety and Availability of Virtual Balises: The SISTER Project. |
| Record Nr. | UNINA-9910619277403321 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Leveraging applications of formal methods, verification and validation, adaptation and learning. Practice : 11th international symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings, Part IV / / Tiziana Margaria-Steffen, Bernhard Steffen, editors
| Leveraging applications of formal methods, verification and validation, adaptation and learning. Practice : 11th international symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, proceedings, Part IV / / Tiziana Margaria-Steffen, Bernhard Steffen, editors |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (431 pages) |
| Disciplina | 005.14 |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer software - Verification
Formal methods (Computer science) |
| ISBN | 3-031-19762-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Introduction -- Organization -- Contents - Part IV -- Digital Twin Engineering -- Engineering of Digital Twins for Cyber-Physical Systems -- 1 Introduction -- 2 Contributions -- 3 Concluding Remarks -- References -- Towards Requirements Engineering for Digital Twins of Cyber-Physical Systems -- 1 Introduction -- 2 Context -- 3 Requirements Engineering for Digital Twins -- 3.1 Requirements Elicitation -- 3.2 Requirements Specification and Modeling -- 3.3 Requirements Verification and Validation -- 4 Common DT Requirements -- 4.1 Data Synchronization Between DT and CPS -- 4.2 Modeling Paradigms and Model Fidelity of DT Models -- 4.3 Extra-functional Requirements -- 4.4 DT Evolution -- 4.5 RE for Dealing with Uncertainty -- 4.6 Requirements Engineering for AI for DT -- 4.7 AI for RE for DT -- 5 State of the Art -- 6 Conclusion -- References -- Digital Twins for Organ Preservation Devices -- 1 Introduction -- 2 Digital Twins -- 2.1 Aims and Benefits -- 2.2 Challenges -- 2.3 Medical Applications -- 3 Medical Devices -- 3.1 Challenges -- 3.2 Organ Preservation -- 4 Case Study: ScubaTx™ Organ Preservation Device -- 4.1 The Device -- 4.2 The Software -- 4.3 Challenges -- 5 Discussion -- 5.1 Beyond Organ Preservation -- References -- Using Digital Twins in the Development of Complex Dependable Real-Time Embedded Systems -- 1 Introduction -- 2 The DTiL-RTES Framework -- 2.1 Design Philosophy -- 2.2 DTiL-RTES Overview and Components -- 2.3 Intended Use and Overhead -- 3 ETM Modelling and Refinement -- 3.1 Execution Time Model -- 3.2 Offline Profiling of CRP Model -- 3.3 Prediction Error -- 3.4 Continuous Refinement Through Naive Feedback -- 3.5 Model Refinement Through Condition-Based Model Rebuilding -- 4 Evaluation -- 4.1 Evaluation Setup -- 4.2 Modelling and Residual Error Evaluation.
4.3 Evaluation of Model Refinement and Performance Improvement -- 4.4 Discussion on Safety Challenges -- 5 Related Work -- 5.1 Timing Prediction for Multi-core Real-Time Embedded Systems -- 5.2 Execution Time Modelling -- 6 Conclusion -- References -- Towards Reactive Planning with Digital Twins and Model-Driven Optimization -- 1 Introduction -- 2 Background and Running Example -- 2.1 Automated Planning and Model-Driven Optimization -- 2.2 Digital Twins -- 3 Reactive Planning Framework -- 3.1 Reactive Planning Architecture -- 3.2 Reactive Planning Strategies -- 3.3 Prototypical Implementation -- 3.4 Demonstration Using the Stack Example -- 4 Evaluation -- 4.1 Case Study Setup -- 4.2 Case Study Results -- 4.3 Discussion -- 4.4 Threats to Validity -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Digital Twin Reconfiguration Using Asset Models -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries -- 3.1 Knowledge Bases -- 3.2 Asset Modelling -- 3.3 Simulation Units -- 4 Semantically Lifted Co-simulation -- 5 Structural Reconfiguration in SMOL -- 6 Conclusion -- References -- Formally Verified Self-adaptation of an Incubator Digital Twin -- 1 Introduction -- 2 Background -- 2.1 Notation -- 2.2 Incubator -- 2.3 Flow* Verified Integration -- 2.4 Verified Monitoring -- 3 Formally Verified Self-Adaptation -- 3.1 Incubator Self-Adaptation Loop -- 3.2 Verified Monitoring Architecture for Safe Self-Adaptation -- 3.3 Uncertainty Calibration -- 3.4 Self-adaptation Monitoring and Enforcement -- 4 Incubator Self-adaptation Verification Results -- 4.1 System Setup -- 4.2 Safety Properties -- 4.3 Self-adaptation Results -- 4.4 Repairing the Loop -- 5 Conclusion -- References -- Adaptive Data-driven Predictor of Ship Maneuvering Motion Under Varying Ocean Environments -- 1 Introduction -- 2 Related Work -- 2.1 Incremental Learning. 2.2 Transfer Learning -- 3 Methodology -- 3.1 Gaussian Process Regression -- 3.2 Predictive Anomaly Detection -- 4 Experiment Results -- 4.1 Experiment Setup -- 4.2 Results Analysis -- 5 Conclusion -- References -- Robust Adaptive Back-Stepping Control Approach Using Quadratic Lyapunov Functions for MMC-Based HVDC Digital Twins -- 1 Introduction -- 2 System Description of MMC -- 3 Modeling of the Proposed Adaptive Backstepping Control -- 3.1 Output Current Control -- 3.2 Other Controlling Loops -- 4 Studied HVDC Digital Twin -- 5 Effectiveness of the Proposed Control Method -- 6 Conclusion -- References -- Data-Driven Reachability Analysis of Digital Twin FMI Models -- 1 Introduction -- 2 Preliminaries and Problem Statement -- 2.1 Reachability Analysis and JuliaReach -- 2.2 Co-simulation and Functional Mock-Up Interface -- 2.3 Problem Statement -- 3 Robust Convex Programs -- 4 Simulation-Based Reachability Algorithm -- 4.1 Reachable Set Computation -- 4.2 Lipschitz Constant Estimation via Extreme Value Theorem -- 4.3 Extension to Other Modelling Formalisms -- 5 Validation Exercises -- 5.1 Sampling-Based Lipschitz Constant Estimation -- 5.2 Reachable Set Computation for Linear Systems -- 5.3 Reachable Set Computation for a Nonlinear System -- 6 Conclusions and Future Work -- References -- Towards Secure Digital Twins -- 1 Introduction -- 2 Related Work -- 3 Security Challenges -- 3.1 Bandwidth Sniffing -- 3.2 Data Injection -- 3.3 Data Delay -- 3.4 Model Corruption -- 4 Mitigations -- 4.1 Fragmentation and Data Padding -- 4.2 Signatures and Tokens -- 4.3 Threshold Monitoring and Network-Aware Digital Twin Models -- 4.4 Model Integrity Checks -- 5 Case Study -- 5.1 Physical Twin -- 5.2 Digital Twin -- 5.3 Example Security Challenges -- 6 Open Problems -- 7 Concluding Remarks -- References -- Digital Thread in Smart Manufacturing. Digital Thread in Smart Manufacturing -- 1 Motivation and Goals -- 2 Overview of Contributions -- References -- Integrating Wearable and Camera Based Monitoring in the Digital Twin for Safety Assessment in the Industry 4.0 Era -- 1 Introduction -- 2 Related Work -- 3 Architecture Overview -- 3.1 Wearable Node -- 3.2 HPE Subsystem -- 4 Application Scenario -- 5 Conclusions -- References -- Model-Driven Engineering in Digital Thread Platforms: A Practical Use Case and Future Challenges -- 1 Introduction -- 2 Industrial Use-Case: Safe Operation of Machines -- 2.1 Architecture of the Use Case -- 2.2 The IT Ecosystem: Tools and Technologies -- 3 Access Control Using Attribute Based Encryption -- 3.1 Bilinear Map -- 3.2 Decision Tree -- 3.3 Our Construction -- 4 Conclusions and Reflections -- References -- Trust and Security Analyzer for Collaborative Digital Manufacturing Ecosystems -- 1 Introduction -- 2 Related Work -- 3 Architecture of Digital Thread Connector -- 4 Initial Implementation -- 5 Conclusion -- References -- DISTiL: DIStributed Industrial Computing Environment for Trustworthy DigiTaL Workflows: A Design Perspective -- 1 Introduction -- 1.1 Motivation -- 1.2 Impact for Smart Manufacturing -- 2 DISTiL Design Requirements and Features -- 3 Architecture Design -- 3.1 Distributed Data Layer -- 3.2 Trust-Overlay -- 3.3 Resource Orchestration andProvisioning -- 3.4 Use Case Scenario: Collaborative Predictive Maintenance -- 4 Discussion and Next Steps -- References -- Using Model Selection and Reduction to Develop an Empirical Model to Predict Energy Consumption of a CNC Machine -- 1 Introduction -- 2 Literature Review -- 3 Methodology -- 4 Case Study -- 5 Model Development -- 5.1 Data Preparation -- 5.2 Data Analysis -- 5.3 Data Modelling -- 6 Discussion -- References. Crazy Nodes: Towards Ultimate Flexibility in Ubiquitous Big Data Stream Engineering, Visualisation, and Analytics, in Smart Factories -- 1 Introduction -- 1.1 Reconfigurable Manufacturing -- 1.2 Framework Overview -- 1.3 Paper Structure -- 2 Service and Crazy Nodes -- 2.1 Crazy Nodes -- 2.2 Towards the Cloud -- 3 Proof of Concept -- 4 Conclusions -- References -- Formal Methods for DIStributed COmputing in Future RAILway Systems -- Formal Methods for Distributed Control Systems of Future Railways -- 1 Motivations and Goals -- 2 Contributions -- References -- Safe and Secure Future AI-Driven Railway Technologies: Challenges for Formal Methods in Railway -- 1 Introduction -- 2 Certified Verification of Railway Designs -- 2.1 Automated Verification -- 2.2 Trustworthy and Certifiable Verification -- 2.3 Explainable Verification -- 2.4 Standardisation -- 3 Formal Modelling and Analysis for the Railway Domain -- 3.1 Domain Specific Technology and Usability -- 3.2 Standardised Reference Architectures -- 3.3 Digital Railway Innovations -- 4 Formal Methods for AI -- 4.1 Guaranteeing Safety Behaviour -- 4.2 Learning Formal Models of Railway Behaviour -- 4.3 AI for Monitoring and Maintenance -- 4.4 AI for Optimisation in Scheduling and Design -- 5 Conclusion and Further Work -- References -- Future Train Control Systems: Challenges for Dependability Assessment -- 1 Introduction -- 2 Context -- 2.1 Future Railway Systems -- 2.2 Uncertainty -- 2.3 Dependability Attributes -- 3 Model-Based Evaluation of Dependability -- 3.1 Proposed Modelling Frameworks -- 4 Survey of Railway Case Studies -- 4.1 Performability Evaluation of the ERTMS/ETCS - Level 3 -- 4.2 Safety Evaluation of Moving Block Systems by Statistical Model Checking -- 4.3 Train-to-Train Communication Modeling -- 4.4 Modelling Uncertainty in Satellite Localisation. 4.5 Safety and Availability of Virtual Balises: The SISTER Project. |
| Record Nr. | UNISA-996495569503316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
