Formal methods for industrial critical systems : 27th International Conference, FMICS 2022, Warsaw, Poland, September 14-15, 2022, proceedings / / Jan Friso Groote, Marieke Huisman (editors)

• Record Nr.: UNISA996490368003316
• Pubbl/distr/stampa: Cham, Switzerland : , : Springer, , [2022]; ©2022
• ISBN: 3-031-15008-2
• Descrizione fisica: 1 online resource (246 pages)
• Collana: Lecture notes in computer science ; ; 13487
• Disciplina: 004.0151
• Soggetti: Formal methods (Computer science); Software engineering
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Intro -- Preface -- Organization -- Contents -- Invited Keynote Talks -- Reinforcement Learning with Guarantees that Hold for Ever -- 1 Learning from Rewards -- 2 Learning with -Regular Objectives -- 2.1 Good-for-MDP Automata -- 2.2 From GFM Büchi Automata to Reachability and RL -- 3 Related Work -- References -- Supporting Railway Innovations with Formal Modelling and Verification -- References -- Certification -- Formal Monotony Analysis of Neural Networks with Mixed Inputs: An Asset for Certification -- 1 Introduction -- 2 Certification Preamble -- 3 Related Work -- 4 Monotony Analysis -- 4.1 Goal of the Analysis -- 4.2 MILP Formulation -- 4.3 Verification Procedure -- 5 Case Study: Braking Distance Estimation -- 5.1 Description of the Case Study -- 5.2 Experimentation -- 6 Conclusion -- References -- Generating Domain-Specific Interactive Validation Documents -- 1 Introduction and Motivation -- 2 Validation Workflow -- 3 Static VisB HTML Export -- 4 Dynamic HTML Export: Code Generation to HTML and JavaScript -- 4.1 Graphical User Interface -- 4.2 Applicability of JavaScript Code Generation -- 5 Case Studies -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Deductive Verification of Smart Contracts with Dafny -- 1 Introduction -- 2 Verification of Closed Smart Contracts -- 3 Verification Under Adversarial Conditions -- 3.1 Aborting a ; Computation -- 3.2 Reasoning with Arbitrary External Calls -- 4 Conclusion -- References -- Industrial Use Cases -- Towards Reusable Formal Models for Custom Real-Time Operating Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Core Components of Real-Time Operating Systems -- 2.2 Uppaal Timed Automata -- 3 Related Work -- 4 Reusable Formal Models for Custom RTOS -- 4.1 Formalization of Tasks -- 4.2 Formalization of Cyclic Handlers -- 4.3 Events and Timing Behavior.; 4.4 Configurable Formal Scheduler Model -- 4.5 Modeling Sensor Inputs and Communication -- 5 Case Study: Search and Rescue Robots -- 6 Conclusion -- References -- Formal Verification of an Industrial UML-like Model using mCRL2 -- 1 Introduction -- 2 Cordis Models -- 2.1 Class Diagrams -- 2.2 State Machine Diagrams -- 3 Cylinder -- 4 Model Checking Cordis Models Using mCRL2 -- 4.1 Translation to mCRL2 -- 4.2 Formal Verification of Requirements -- 4.3 Results -- 5 Discussion -- 6 Concluding Remarks -- References -- Chemical Case Studies in KeYmaera X -- 1 Introduction -- 2 Background -- 2.1 Differential Dynamic Logic -- 2.2 KeYmaera X -- 3 Results -- 3.1 Controlled Irreversible Reactions -- 3.2 Uncontrolled Reversible Reactions -- 4 Related Work -- 5 Conclusion -- References -- Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining -- 1 Introduction -- 2 Related Work -- 3 Identification of Capacity Bottlenecks -- 3.1 Method -- 3.2 Results -- 4 Analysing Delay Propagations -- 4.1 Goals and Overview -- 4.2 Episode Mining -- 4.3 Algorithm and Implementation -- 4.4 Adaptations -- 5 Evaluation Results -- 6 Conclusions and Outlook -- References -- Testing and Monitoring -- Test Suite Augmentation for Reconfigurable PLC Software in the Internet of Production -- 1 Introduction -- 1.1 Limitations and Contributions -- 2 Related Work -- 3 Methodology -- 3.1 Intermediate Representation -- 3.2 Bounded Symbolic Execution -- 3.3 Shadow Symbolic Execution -- 4 Evaluation -- 5 Conclusion -- References -- Monitoring of Spatio-Temporal Properties with Nonlinear SAT Solvers -- 1 Introduction -- 2 Preliminaries -- 3 Running Example -- 3.1 Formalization of Road Traffic Rules with LTL MS -- 3.2 Scenario and Trace Encoding (Static and Dynamic Objects) -- 4 Monitoring Model Construction -- 5 Empirical Evaluation -- 6 Related Work.; 7 Conclusion and Future Work -- References -- Model-Based Testing of Internet of Things Protocols -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries -- 2.1 Internet of Things -- 2.2 Model-Based Testing -- 2.3 Axini Modeling Platform (AMP) -- 3 MBT in the Context of IoT -- 3.1 IoT Testing Challenges -- 3.2 Positioning MBT in IoT -- 4 The AMP MBT Environment to Test BLE IoT Systems -- 4.1 SUT -- 4.2 Model Creation -- 4.3 AML Model Example -- 4.4 Adapter -- 5 Testing BLE Using AMP -- 5.1 Assumption -- 5.2 Test Generation Configurations -- 5.3 Conformance Experiment -- 5.4 Model Assumption Experiment -- 6 Discussion -- 7 Conclusion -- 7.1 Future Work -- References -- Methodology -- Formally Verifying Decompositions of Stochastic Specifications -- 1 Introduction -- 2 Problem Illustration -- 3 A Theory for Specifying Stochastic Behavior -- 3.1 Traces and Behaviors -- 3.2 Specifications -- 3.3 Trace Automata -- 3.4 Probabilistic Automaton Contracts -- 4 Verification of Refinement -- 5 Case Study -- 6 Related Work -- 7 Conclusions -- References -- Verification of Behavior Trees using Linear Constrained Horn Clauses -- 1 Introduction -- 2 Related Works -- 3 Preliminaries -- 3.1 Behavior Trees -- 3.2 Constrained Horn Clauses -- 4 Encoding of Behavior Trees -- 4.1 Idea -- 4.2 Action Node -- 4.3 Condition Node -- 4.4 Sequence Node -- 4.5 Sequence Node with Memory -- 4.6 Selector Node -- 4.7 Parallel Node -- 4.8 Root Node -- 4.9 Safety ; Property -- 4.10 Environment -- 5 Experiments -- 5.1 Benchmark -- 5.2 Discussion -- 6 Conclusion and Outlook -- References -- A Multi-level Methodology for Behavioral Comparison of Software-Intensive Systems -- 1 Introduction -- 2 Background -- 2.1 Software Behavior -- 2.2 State Machines -- 2.3 State Machine Comparison -- 3 Behavioral Comparison Methodology -- 3.1 Level 1: Model Set Variants.; 3.2 Level 2: Model Set Variant Relations -- 3.3 Level 3: Model Set Variant Differences -- 3.4 Level 4: Model Variants -- 3.5 Level 5: Model Variant Relations -- 3.6 Level 6: Model Variant Differences -- 4 Evaluation -- 4.1 Case Study 1: Legacy Component Technology Migration -- 4.2 Case Study 2: System Behavior Matching Recipe -- 5 Conclusions and Future Work -- References -- Author Index.

HCI International 2024 – Late Breaking Papers : 26th International Conference on Human-Computer Interaction, HCII 2024, Washington, DC, USA, June 29 – July 4, 2024, Proceedings, Part IV / / edited by Jessie Y. C. Chen, Gino Fragomeni, Norbert A. Streitz, Shin'ichi Konomi, Xiaowen Fang

• Record Nr.: UNISA996635671403316
• Autore: Chen Jessie Y. C
• Pubbl/distr/stampa: Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2025
• ISBN: 9783031768125; 3031768124
• Edizione: [1st ed. 2025.]
• Descrizione fisica: 1 online resource (464 pages)
• Collana: Lecture Notes in Computer Science, , 1611-3349 ; ; 15377
• Altri autori (Persone): FragomeniGino; StreitzN. A (Norbert A.); KonomiShinʾichi; FangXiaowen
• Disciplina: 005.437; 004.019
• Soggetti: User interfaces (Computer systems); Human-computer interaction; User Interfaces and Human Computer Interaction
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Nota di contenuto: Virtual Experiences in XR and the Metaverse: Study and Development of Machine Learning Models Designed for Extended Reality Interactivity in Real-Time -- Optimizing AR Application Testing: Integrating Metamorphic Testing to Address Developer and End-User Challenges -- Comparing Vibrotactile and Visual Feedback in Virtual Reality Motion Guidance: An Investigation on Workload and Performance -- Improving Virtual Workspaces Based on Sense of Embodiment -- Working in Extended Reality: A Study on the Relationship Between Concentration and Work in Immersive Environments -- Influence of Color on Asthenopia of VR based on Real-time Teleoperating Lunar Rover -- Effects of Avatar Design on Alarm Resolution in a Virtual Reality Physical Security Scenario -- Enhancing Augmented Reality (MAR) Interaction Experience: A Design Framework Grounded in User Mental Model Construction -- Advantages of Virtual Reality Tool for Helping Personal Sketch Modeling -- Effects of Redirected Walking on Cybersickness in an Applied Virtual Environment -- Towards a VR Environment for Desensitization of Ecological Anxiety -- Are We There Yet? Unravelling Usability Challenges and Opportunities in Collaborative Immersive Analytics for Domain Experts -- The Effect of Visual Design Using Biomorphic Designs on Walking Behavior in Virtual World -- Interactive Visual Narrative (IVN) Model: Understanding Discourse Production in IVNs -- Effects of Basic Movement Characteristics and Cognitive Load on Performance Indicators in VR-IADLs -- Factors Influencing the Purchase Intention of Consumer VR All-in-one Headsets -- HoloCook: A Real-Time Remote Mixed Reality Cooking Tutoring System -- Conceptual Design Ease of Use MR-PACS. Playing Experiences: Alien Mystery Scavenger Hunt: Enhancing Intergenerational Interaction with Physical Web Technologies through Location-Based Games -- Augmented Motion Representation Learning Based on Virtual Reality Sports Game Review Data -- Exploring Virtual Chess Personalities: Analyzing Class-C Players vs. Nimzowitsch and Fine Virtual Grandmasters -- Storytelling, Worlds and Game Design: Viewer Experience and Interaction In “Sky, Children of the Light” -- A Review of Cultural Impact on Children's Play Perception and Digital Games -- Head and Shoulder (e)Sports Event Organization Tools: A User-Based Study -- SDG Quest: Leveraging Mobile Game-Based Learning to Foster Environmental, Social, and Economic Sustainable Development Goals -- Automated Facial Mark Creating Systems Replace Classical Geometric Morphometrics: An Example of How New Technology Can and Should Drive Avatar Creation in a Game Development Pipeline -- UBI Journey: A Tool Against University Student Social Isolation -- AI-Enhanced Tools for Cross-Cultural Game Design: Supporting Online Character Conceptualization and Collaborative Sketching.
• Sommario/riassunto: This nine-volume set LNCS 15473-15482 constitutes the proceedings of the 26th International Conference, HCI International 2023, in Washington, DC, USA, in June/July 2024. For the HCCII 2024 proceedings, a total of 1271 papers and 309 posters was carefully reviewed and selected from 5108 submissions. Additionally, 222 papers and 104 posters are included in the volumes of the proceedings published after the conference, as “Late Breaking Work”. These papers were organized in the following topical sections: HCI Theories, Methods and Tools; Multimodal Interaction; Interacting with Chatbots and Generative AI; Interacting in Social Media; Fintech, Consumer Behavior and the Business Environment; Design for Health and Wellbeing; Ergonomics and Digital Human Modelling; Virtual Experiences in XR and the Metaverse; Playing Experiences; Design for Learning; New Cultural and Tourism Experiences; Accessibility and Design for All; Design for ; Older Adults; User Experience Design and Evaluation: Novel Approaches and Case Studies; Safety, Security and Privacy; HCI in Automated Vehicles and Automotive; HCI in Aviation, Transport and Safety; Human-Centered AI; AI for Decision Making and Sentiment Analysis.