Software Engineering and Formal Methods: 19th International Conference, SEFM 2021, Virtual Event, December 6–10, 2021, Proceedings

Description

This book constitutes the refereed proceedings of the 19th International Conference on Software Engineering and Formal Methods, SEFM 2021, held as a virtual event, in December 2021. The 22 full papers presented together with 4 short papers were carefully reviewed and selected from 86 submissions. Also included are 2 invited talks and an abstract of a keynote talk. The papers cover a large variety of topics, including testing, formal verification, program analysis, runtime verification, meta-programming and software development and evolution. Chapter 'Configuration Space Exploration for Digital Printing Systems' is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. Preface Organization Controller Synthesis for Adaptive Mobile Robots. Abstractions, All Change!? (Keynote Abstract) Contents Invited Papers RoboWorld: Where Can My Robot Work? 1 Introduction 2 RoboWorld Syntax 3 RoboWorld Semantics 4 Tool 5 Verification: Testing 6 Conclusion References Validating Safety Arguments with Lean 1 Introduction 2 Background 2.1 Models 2.2 Assurance Case Strategy Formalization 3 Lean-Validated Strategies 3.1 A Strategy Validation Workflow 3.2 Formalizing Models 3.3 Formalizing Strategies 3.4 Proof Automation 3.5 Application to the FCS 3.6 Theorem Proving for AC Validation: Challenges 4 Towards a Black-Box Usage of Lean in AC Validation 4.1 Integrating Lean with MMINT-A 4.2 FCS Strategy Decomposition Example 4.3 Discussion 5 Related Work 6 Conclusion References Run-time Analysis and Testing Runtime Enforcement with Reordering, Healing, and Suppression 1 Introduction 2 Models 3 Enforcement Techniques 3.1 Overview 3.2 Enforcement Monitor 3.3 Enforcement Trend 3.4 Characteristics 4 Case Study 5 Tool Support and Experiments 5.1 Tool Support 5.2 Experiments 5.3 Comparison 6 Related Work 7 Concluding Remarks References Monitoring First-Order Interval Logic 1 Introduction 2 Preliminaries 3 A First-Order Interval Logic 4 The Monitoring Algorithm 5 Alternative Algorithm Translating to Past First-Order LTL 6 Implementation 6.1 Experiments 7 Conclusion References Exhaustive Property Oriented Model-Based Testing with Symbolic Finite State Machines 1 Introduction 2 Symbolic Finite State Machines, Simulations, Equivalence Classes, and FSM Abstractions 3 An Exhaustive Property-Based Testing Strategy 4 Conclusion References nfer – A Tool for Event Stream Abstraction 1 Introduction 2 Writing Nfer Rules 3 Nfer's Architecture 4 Comparison with TeSSLa 5 Conclusion References Mining Shape Expressions with ShapeIt 1 Introduction 2 Shape Expressions 3 ShapeIt Architecture, Methods and Implementation 4 Evaluation 5 Conclusion and Future Work References Security and Privacy Refining Privacy-Aware Data Flow Diagrams 1 Introduction 2 Preliminaries 3 Refining B-DFDs and PA-DFDs 3.1 Refinement of Attributed Multigraphs 3.2 B-DFD Refinement 3.3 PA-DFD Refinement 4 DFD Refinery 5 Case Study 6 Related Work 7 Conclusions A Additional Transformation Rules References Hybrid Information Flow Control for Low-Level Code 1 Introduction 2 Related Work 3 Overview 4 Dynamic Semantics 4.1 Monitor Non-interference 5 Static Semantics 5.1 Soundness 6 Conclusions References Upper Bound Computation of Information Leakages for Unbounded Recursion 1 Introduction 2 Related Work 3 Foundations 4 Preprocessing 5 Bit Dependency Graph 5.1 Handling Functions 5.2 From Bit Dependency Graph to Leakage 5.3 Summary Function Handler 6 Increasing the Precision 7 Evaluation 8 Conclusion and Future Work References On the Security and Safety of AbU Systems 1 Introduction 2 Related Work 3 Attribute-Based Memory Updates in Short 3.1 AbU Syntax and Semantics 3.2 AbU in Action: an IoT Example 4 Behavioral Equivalences for AbU Systems 4.1 A Bisimulation for Security 4.2 A Bisimulation for Safety 5 Checking Security and Safety of AbU Systems 5.1 Verifying Security 5.2 Verifying Safety 5.3 On the Completeness of the Verification Mechanisms 6 Dealing with Implicit Interactions 7 Conclusion References Parallel Composition/CSP and Probabilistic Reasoning Parallelized Sequential Composition and Hardware Weak Memory Models 1 Introduction 2 Foundations of Instruction Reordering 2.1 Reorderings 2.2 Forwarding 2.3 Strengthening Memory Models 3 An Imperative Language with Instruction Reordering 3.1 Syntax 3.2 Operational Semantics 4 Hardware Weak Memory Models 4.1 Total Store Order (TSO) 4.2 Release Consistency 4.3 Arm Version 8 4.4 RISC-V 5 Related Work 6 Conclusion References Checking Opacity and Durable Opacity with FDR 1 Introduction 2 Example: (Durable) Transactional Mutex Lock 3 Opacity and Durable Opacity 4 Proving Opacity and Durable Opacity 5 CSP and FDR Models 5.1 Overview of CSP 5.2 Setup and TMS2 Shared Memory 5.3 TMS2 Model 5.4 Encoding STM Implementations 6 Evaluation and Experiments 7 Related Work 8 Conclusions A Full (d)TMS2 Automata B (d)NOrec References Translation of CCS into CSP, Correct up to Strong Bisimulation 1 Introduction 2 CCS, CSP, Correct Translations: a Brief Overview 2.1 CCS 2.2 CSP 2.3 Correct Translations 3 Intuitions of the Translation 4 From CCS to CCSTau 5 CCSTau Transformations 6 From CCSTau to CSP 7 Correctness of the Translation 8 Alternative Translation, Correct up to Failure Equivalence 9 Structural Properties of the Translation 10 Conclusion and Future Work References Probabilistic BDI Agents: Actions, Plans, and Intentions 1 Introduction 2 Background 2.1 BDI Agents 2.2 Bigraphs 3 Probabilistic Extension of CAN Semantics 3.1 Probabilistic Action Outcomes 3.2 Plan Selection and Its Probabilistic Extension 3.3 Intention Selection and Its Probabilistic Extension 3.4 Situation-Aware Distributions for Plan and Intention Selection 4 Evaluation 4.1 Smart Manufacturing Example 4.2 Agent Design 4.3 Plan and Intention Selection Strategies 4.4 Plan and Intention Selection Analysis 4.5 Action Outcome Analysis 5 Related Work 6 Conclusions References A Debugger for Probabilistic Programs 1 Introduction 2 Probabilistic Programs 3 Weakest Preexpectations 4 Loop Iteration Limits 5 Weakest Preexpectations at Intermediate Execution States 5.1 Execution History of a Program 6 Implementation References Verification and Synthesis Verification of Programs with Exceptions Through Operator Precedence Automata 1 Introduction 2 Background: Operator Precedence Languages 3 Background: Precedence Oriented Temporal Logic 4 Model Checking OPA 5 Modeling Procedural Programs 6 Experiments 6.1 Discussion 7 Conclusions References Counterexample Classification 1 Introduction 1.1 Running Example 2 Background 3 Counterexample Classification 3.1 Classes and Classifications 3.2 The Counterexample Classification Problem 3.3 Solvability 3.4 Uniqueness of Solutions 4 Classification Method 4.1 Algorithm Overview 4.2 Optimizations 4.3 Solution to the Running Example 5 Implementation and Case Studies 5.1 Implementation 5.2 Case Studies: Needham-Schroeder 6 Related Work 7 Conclusion and Future Work References Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines 1 Introduction 2 Preliminaries 2.1 Computation Tree Logic 2.2 Recursive State Machines 3 Ternary RSM Model Checking 3.1 Local Deduction 3.2 Contextualization of Components 3.3 Global Deduction 3.4 Exhaustive Approach to RSM Model Checking 4 Lazy RSM Model Checking 4.1 Lazy Contextualization 4.2 Lazy Approach to RSM Model Checking 5 Implementation and Evaluation 5.1 Scalability Experiment 5.2 PuMoC Benchmark Set 5.3 Interprocedural Static Analysis for Java Programs 6 Conclusion and Discussion References Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis 1 Introduction 2 Preliminaries 2.1 Temporal Logics 2.2 Automata 2.3 Model Checking, Realizability, and Synthesis 3 LTLEBR+P with Fairness, Assumptions, and Guarantees 3.1 Expressiveness of GR-EBR 3.2 An Example 4 A Framework of Safety Reductions for LTL+P Realizability 5 A Safety Reduction for GR-EBR 5.1 Construction of the Automaton with a GR(1) Condition 5.2 Degeneralization 5.3 Reduction to Safety for Reactivity(1) Objectives 6 Experimental Evaluation 7 Conclusions References TACoS: A Tool for MTL Controller Synthesis 1 Introduction 2 The MTL Synthesis Problem 3 Approach 4 Evaluation 5 Conclusion References Emerging Domains Lightweight Nontermination Inference with CHCs 1 Introduction 2 CHCs, Recurrence Sets and Preconditions 3 CHC Transformations and Their Roles in Non-termination Analysis 4 An Algorithm for Conditional Non-termination 5 Implementation and Experiments 6 Related Work 7 Concluding Remarks References A Denotational Semantics of Solidity in Isabelle/HOL 1 Introduction 2 Semantics 2.1 Value Types 2.2 Stores and Reference Types 2.3 Expressions 2.4 Statements 3 Compliance to the Official Solidity Implementation 3.1 Results 4 Verified Constant Folding 5 Memory Optimization 6 Related Work 7 Conclusion References Configuration Space Exploration for Digital Printing Systems 1 Introduction 2 Finishers in the Digital Printing Domain 2.1 Perfect Binding 3 CSX 3.1 Configurations and Jobs 3.2 Exploration and Validation 4 Denotational Semantics 5 Implementation 6 Evaluation 7 Related Work 8 Conclusions References Bit-Precise Verification of Discontinuity Errors Under Fixed-Point Arithmetic 1 Introduction 2 Preliminaries 2.1 Fixed-Point Arithmetic 2.2 Numerical Errors 2.3 Fixed-Point Programs 3 Propagation of Discontinuity Errors 3.1 Motivating Example 3.2 Computing the Discontinuity Error 4 Program Analysis 4.1 Verification Workflow 4.2 Program Transformation 5 Experimental Evaluation 6 Related Work 7 Conclusion and Future Directions References Machine Learning and Cyber-Physical Systems OSIP: Tightened Bound Propagation for the Verification of ReLU Neural Networks 1 Introduction 2 Preliminaries 3 OSIP: Tightened Bound Propagation 4 Implementation and Evaluation 5 Conclusions References Active Model Learning of Stochastic Reactive Systems 1 Introduction 2 Preliminaries 3 Queries-Based Learning of SMMs via Sampling 3.1 Basics 3.2 Queries 3.3 Learner 3.4 Implementation 3.5 Analysis of L*SMM 4 Evaluation 5 Related Work 6 Conclusion References Mixed-Neighborhood, Multi-speed Cellular Automata for Safety-Aware Pedestrian Prediction 1 Introduction 2 Related Work 3 Preliminaries 3.1 Cellular Automaton (CA) 3.2 Cellular Automaton for Pedestrian Prediction 3.3 Initialization of c0 4 Transition Rule 4.1 Variable Update-Rate 4.2 Multiple Neighborhood Usage 4.3 Cardinal Directions Vectorization 4.4 Over-Propagation 5 Implementation 5.1 Performance Implications of Environment Density 5.2 Performance Compared to Simple Cell-Growth Algorithm 6 Discussion 7 Conclusion References Author Index