Dependable Software Engineering. Theories, Tools, and Applications: 7th International Symposium, SETTA 2021, Beijing, China, November 25–27, 2021, Proceedings

Preface
Organization
Abstracts of Keynote Speeches
Mechanically Finding the Right Probabilities in Markov Models
A New Approach for Active Automata Learning Based on Apartness
Enterprise-Scale Static Analysis: A Pinpoint Experience
Contents
Systems Development
Translating a Large Subset of Stateflow to Hybrid CSP with Code Optimization
1 Introduction
2 Hybrid CSP
3 A Brief Tour of Stateflow Semantics
3.1 States
3.2 Transitions
3.3 Junctions
3.4 State Lifecycle
3.5 Events and Temporal Events
3.6 Early Return
3.7 Data and Messages
3.8 Functions and Graphical Functions
3.9 Continuous Evolution
4 Translation from Stateflow
4.1 Variables
4.2 States
4.3 Transitions and Junctions
4.4 Events
4.5 Order of Execution of Charts
4.6 Translation of Continuous Evolution
5 Code Optimization
5.1 Inlining of Procedures
5.2 Peephole Optimization
5.3 Constant Propagation
5.4 Dead Code Elimination
6 Evaluation
6.1 Benchmarks
6.2 Case Studies
7 Related Work
8 Conclusion and Future Works
References
DeepGlobal: A Global Robustness Verifiable FNN Framework
1 Introduction
2 Background
2.1 Feed Forward Neural Networks
2.2 Adversarial Dangerous Regions
3 Naive Rule-Generation
4 Sliding Door Network for Feasible Rule-Generation
4.1 Sliding Door Network
4.2 Rule-Generation for SDN
5 Selection Approach for Generated Rules
5.1 Pre-processing of Generated Rules
5.2 Real Boundaries Selection Approach
6 Experiments
6.1 Effectiveness of Reducing Rule-Generation Cost
6.2 Feasibility of Global Verification
7 Conclusion
References
Leveraging Event-B Theories for Handling Domain Knowledge in Design Models
1 Introduction
2 Event-B: A Refinement and Proof-Based Formal Method
2.1 Core Event-B
2.2 Event-B Extensions with Theories
3 Related Works
4 Domain Knowledge in State-Based Formal Methods: The Case of Event-B
5 Ontologies as Event-B Theories
6 Application to the Design of Critical Interactive Systems
6.1 The TCAS Case Study
6.2 A Domain Ontology for the Critical Interactive Systems
6.3 Ontology-Based Annotation of TCAS Design Model
7 Assessment
8 Conclusion and Future Work
References
Program Analysis and Verifiation
Reasoning About Iteration and Recursion Uniformly Based on Big-Step Semantics
1 Introduction
2 The Technique
2.1 Specifications
2.2 Semantic Derivation and Correctness
2.3 Specification-Aware Inference and Verification
2.4 Soundness
3 Illustrative Example
3.1 Big-Step Semantics of the While Language
3.2 Factorial Program and Its Specification
3.3 Proof of the Factorial Program
3.4 Comparison with Hoare-Style Program Verification
4 Verification of Iterative and Recursive Programs
4.1 Extended While Language and Array-Merging Program
4.2 Eager Functional Language and List-Merging Program
5 On Completeness of the Technique
6 Related Work
7 Future Directions
8 Conclusion
References
Trace Semantics and Algebraic Laws for MCA ARMv8 Architecture Based on UTP
1 Introduction
2 Trace Semantics
2.1 The Syntax of ARMv8
2.2 The Semantic Model
2.3 Trace Semantics
3 Algebraic Properties
3.1 Guarded Choice
3.2 Head Normal Form
3.3 Algebraic Laws
4 Conclusion and Future Work
A Read Function
References
Formal Analysis of 5G AKMA
1 Introduction
2 AKMA in 5G System
2.1 General Architecture
2.2 5G AKMA Protocol
3 Tamarin Prover
3.1 Modeling
3.2 Property Specification
4 Modeling and Specifying Properties of AKMA
4.1 Threat Model
4.2 Modeling the AKMA Service in Tamarin
4.3 Specifying Properties
5 Results and Analysis
5.1 Verification Results and Analysis
5.2 Suggestions
6 Conclusion
References
Verifying the Correctness of Distributed Systems via Mergeable Parallelism
1 Introduction
2 Overview
3 Asynchronous Message Passing Programs
4 Mergeable Message Passing Programs
5 Simplified Reasoning
5.1 Analysis by Inference Rules
5.2 The Soundness of Using Inference Rules
6 Algorithm
6.1 Algorithm_Merging
6.2 Validity of the Algorithm
7 Experimental Evaluation
7.1 Examples
7.2 Experimental Results
8 Related Work
9 Conclusion
References
Testing and Fault Detection
Mutation Testing of Reinforcement Learning Systems
1 Introduction
2 Background
2.1 Reinforcement Learning
2.2 Mutation Testing
3 Mutation Testing Specific to RL Systems
3.1 Element-Level Mutation Operators
3.2 Agent-Level Mutation Operators
3.3 Mutation Testing Framework for RL Systems
4 Mutation Scores Specific to RL Systems
5 Design of Test Environments
6 Evaluation
7 Related Work
7.1 Mutation Testing
7.2 Reinforcement Learning
7.3 AI Safety
8 Conclusion and Future Work
References
AIdetectorX: A Vulnerability Detector Based on TCN and Self-attention Mechanism
1 Introduction
2 Design of AIdetectorX
2.1 Program Representation
2.2 TCN Layer
2.3 Self-attention Layer
2.4 Overview of AIdetectorX
3 Experimental Design
3.1 Evaluation Metrics
3.2 Comparative Vulnerability Detector
3.3 Evaluation Datasets
3.4 Experimental Produce
4 Results and Discussions
4.1 Experiments for Answering RQ1
4.2 Experiments for Answering RQ2
5 Threats to Validity
6 Conclusions
References
MC/DC Test Cases Generation Based on BDDs
1 Introduction
2 Background
2.1 Modified Condition Decision Coverage (MC/DC) Criterion
2.2 Overview on Binary Decision Diagrams (BDDs)
3 Approaches and Algorithm for Test Cases Generation
3.1 Theorems and Definitions for MC/DC in Terms of BDDs
3.2 Algorithm and Heuristics for Test Cases Generation
4 Implementation of MC/DC Test Cases Selection
4.1 Experimental Setup
4.2 Experimental Results
5 Related Work
6 Conclusion and Future Works
References
Software Quality
Predicting and Monitoring Bug-Proneness at the Feature Level
1 Introduction
2 Background and Related Work
2.1 Bug Prediction at Class or File Level
2.2 Bug Prediction at Method Level
2.3 Bug Prediction at Coarse-Grained Level
2.4 Bug Prediction at Other Granularity Levels
3 Study Design
3.1 Feature Identification
3.2 Attributes: Code Metrics
3.3 Labeled Classes: Bug-Prone and Not Bug-Prone Feature
3.4 Machine Learning Algorithms
3.5 Researched Projects
4 Evaluation
4.1 Research Questions
4.2 Prediction Model Development
4.3 Evaluation Method
4.4 Results
5 Threats to Validity
6 Conclusion
References
CSFL: Fault Localization on Real Software Bugs Based on the Combination of Context and Spectrum
1 Introduction
2 Background
2.1 Spectrum-Based Fault Localization
2.2 Context-Based Fault Localization
3 Approach
3.1 Basic Framework
3.2 The Algorithm of Context Analysis
3.3 The Case Study of CSFL
3.4 Time Cost Reduction
4 Evaluation
4.1 Research Questions
4.2 Experimental Subjects
4.3 Implementation Details
4.4 Measurements
5 Results Analysis
5.1 RQ1: How Does CSFL Perform in Locating Real Faults?
5.2 RQ2: How Much Efficiency Has CSFL Improved?
5.3 RQ3: How About the Time Cost of CSFL?
5.4 Threats to Validity
6 Related Work
6.1 Spectrum-Based Fault Localization
6.2 Combination of Context and Spectrum-Based for Fault Localization
7 Conclusion
References
A Distributed Simplex Architecture for Multi-agent Systems
1 Introduction
2 Background
2.1 Simplex Architecture
2.2 Control Barrier Functions
3 Distributed Simplex Architecture
3.1 Baseline Controller
3.2 Decision Module
3.3 Safety Theorem
4 Flocking Case Study
4.1 Synthesis of Control Barrier Function
4.2 Advanced Controller
4.3 Experimental Results
5 Way-Point Case Study
5.1 Experimental Results
6 Microgrid Case Study
6.1 Synthesis of Control Barrier Function
6.2 Advanced Controller
6.3 Experimental Results
7 Related Work
8 Conclusion
References
Satisfiability, Reachability and Model Checking
OURS: Over- and Under-Approximating Reachable Sets for Analytic Time-Invariant Differential Equations
1 Overview of OURS
2 Main Theoretical Features
2.1 EF Based Description of Reachable Set
2.2 RE Based Approximation of Reachable Sets
3 Main Implementation Features
3.1 Inputs and Outputs
3.2 Technical Implementation
3.3 Correctness Analysis of OURS
4 Comparisons with Examples
5 Conclusion
References
ESampler: Efficient Sampling of Satisfying Assignments for Boolean Formulas
1 Introduction
2 Preliminaries
3 Derivation Procedure
3.1 Motivating Example
3.2 Derivation Algorithm
4 ESampler
5 Implementation and Evaluation
5.1 Comparison with QuickSampler
5.2 Comparison with STS
5.3 Comparison with UniGen3
5.4 Execution Time vs Number of Satisfying Assignments
5.5 Testing Uniformity
6 Conclusion
References
API Usage Pattern Search Based on Model Checking
1 Introduction
2 Related Work
3 API Transition System Model
3.1 Class Library API Dependency
3.2 API Transition System
3.3 Constructing API Transition System
4 Formalization of the Matching Rules of Queries
4.1 Semantic Descriptions of Rules
4.2 Characterization of Query Rules by CTL*
5 Evaluation
5.1 Setup
5.2 Results
6 Conclusion
References
Author Index