Formal Methods and Software Engineering : 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings

This book constitutes the proceedings of the 22nd International Conference on Formal Engineering Methods, ICFEM 2020, held in Singapore, Singapore, in March 2021. The 16 full and 4 short papers presented together with 1 doctoral symposium paper in this volume were carefully reviewed and selected from 41 submissions. The papers cover theory and applications in formal engineering methods together with case studies. They also represent the recent development in the use and development of formal engineering methods for software and system development. Preface Organization Contents Safety and Security Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems 1 Introduction 2 Attack-Defence Trees 2.1 The Basic ADTree Model 2.2 Attributes and Agents for ADTrees 2.3 Example: Treasure Hunters 3 AMAS 4 Extending the AMAS Model 5 EAMAS Transformation of ADTrees 5.1 Transformation Patterns 5.2 Adding Node Attributes 6 Experiments 6.1 Case Studies 6.2 Experimentation Setup 6.3 Verifying Correctness 6.4 Playing with Agents Coalitions 6.5 Parameter Synthesis 7 Conclusion and Future Work References Robustness and Failure Detection in Epistemic Gossip Protocols 1 Introduction 2 Related Work 3 Basic Concepts 3.1 Modeling Agent Failure 3.2 Epistemic Logic 4 Analysis of Robustness and Failure Detection 4.1 Properties on Robustness 4.2 Analysis of Failure Detection 5 Conclusions and Future Work References Reasoning with Failures 1 Introduction 2 SIS and FMR 3 Modelling Failures 4 Failure Mode Reasoning 5 Individual Function Blocks 6 FMR in Practice 7 Discussion and Related Works 8 Conclusion References Program Verification Verification of Programs with Pointers in SPARK 1 Introduction 2 Informal Overview of Alias Analysis in SPARK 3 SPARK Language 4 Access Policies, Transformers, and Alias Safety Rules 5 Implementation and Evaluation 6 Related Work 7 Future Work 8 Conclusion A Semantics for SPARK statements References Automated Temporal Verification of Integrated Dependent Effects 1 Introduction 2 Overview 2.1 Integrated Dependent Effects 2.2 Forward Verification 2.3 The T.r.s 3 Language and Specifications 3.1 Target Language 3.2 The Specification Language 3.3 Semantic Model of Effects 4 Automated Verification 5 Effects Inclusion Checker (the T.r.s) 6 Implementation and Evaluation 6.1 Case Studies 6.2 Experimental Results 7 Related Work 7.1 Verification and Expressive Effects 7.2 Efficient Algorithms for Language Inclusion Checking 8 Conclusion References A Reversible Operational Semantics for Imperative Programming Languages 1 Introduction 2 Preliminaries: SIMP 3 RIMP: A Reversible Imperative Language 4 A Program Inverter for RIMP 5 Reversing the Computations in RIMP 6 Related Work 7 Conclusions and Future Work References Parallel Chopped Symbolic Execution 1 Introduction 2 Background 2.1 Parallel Symbolic Execution 2.2 Chopping in Symbolic Execution 3 Illustrative Example 3.1 Prefix Generation in Chopper 3.2 Prefix Generation in PChop 4 Approach 4.1 Prefix Generation 4.2 Parallel Execution 5 Evaluation 5.1 Subjects 5.2 Methodology 5.3 Results 6 Related Work 7 Limitations 8 Conclusions References Formal Methods and Machine Learning PAC Learning of Deterministic One-Clock Timed Automata 1 Introduction 2 Preliminaries 2.1 Deterministic One-Clock Timed Automata 2.2 Exact Learning Algorithm for DOTAs 2.3 PAC Learning of DFA 3 PAC Learning of DOTA 3.1 PAC-Style Correctness 3.2 PAC-Style Equivalence Query 3.3 Sampling Mechanism 3.4 Comparator 3.5 Counterexample Minimization 3.6 The Whole Procedure 4 Extending PAC Learning to Normal Teacher 5 Implementation and Experimental Results 5.1 TCP Protocol 5.2 Random Experiments 6 Related Work 7 Conclusion References Learning Fault Models of Cyber Physical Systems 1 System Description 2 Overview 2.1 Step 1 - Develop Oracles 2.2 Step 2 - Apply Active Automata Learning 2.3 Illustration 3 Implementation 4 Research Questions and Experiments 4.1 How Effective Is Our Approach in Debugging a Real CPS? 4.2 Does Increasing the Size of the Alphabet Increase the Time Overhead Significantly? 4.3 Can Our Approach Effectively Reduce the Length of Discovered Buggy Traces? 4.4 Can Our Approach Find Bugs Effectively? 5 Related Work 6 Conclusion References VARF: Verifying and Analyzing Robustness of Random Forests 1 Introduction 2 Related Work 3 Preliminaries 3.1 Robustness Properties 3.2 Satisfiability Modulo Theories 4 Encoding of Decision Trees and Random Forests 4.1 Decision Tree 4.2 Random Forests Classifier 5 Encoding of Robustness Properties 5.1 Verifying Adversarial Robustness 5.2 Verifying Universal Adversarial Robustness 6 Robust Feature Set and Local Robustness Feature Importance 6.1 Robust Feature Set 6.2 Local Robustness Feature Importance 7 Experiments and Analysis 8 Conclusions and Future Work References Formal Languages Type-Based Declassification for Free 1 Introduction 2 Background: Language and Abstraction Theorem 3 Declassification Policies 4 Type-Based Declassification 4.1 Views and Indistinguishability 4.2 Free Theorem: Typing in the Public View Implies Security 5 Related Work 6 Discussion and Conclusion References Four-Valued Monitorability of -Regular Languages 1 Introduction 2 Preliminaries 3 Four-Valued Monitorability 4 Computing Four-Valued Monitorability 5 State-Level Four-Valued Weak Monitorability 6 Implementation and Experimental Results 7 Related Work 8 Conclusion References Other Applications of Formal Methods Formally Verified Trades in Financial Markets 1 Introduction 1.1 An Overview of Trading at an Exchange 1.2 Our Contribution 1.3 Related Work 1.4 Organization of the Paper 2 Modeling Trades at Exchanges 2.1 Bid, Ask and Limit Price 2.2 Matching Demand and Supply 2.3 Individually Rational Trades 2.4 Fairness in Competitive Markets 2.5 Liquidity and Perceived-Fairness in the Markets 3 Optimizing Trades in Financial Markets 3.1 A Maximum Matching Mechanism 3.2 Trading at Equilibrium Price 4 Conclusion and Future Works References Formalizing the Transaction Flow Process of Hyperledger Fabric 1 Introduction 2 The Architecture of Hyperledger Fabric 2.1 The Central Concepts 2.2 The Transaction Flow 3 Formalizing the Architectural Entities 3.1 Sets and Elements for the Entities 3.2 Inspection and Update of the Entities 3.3 Illustrative Examples 4 Formalizing the Transaction Flow 4.1 Specification of the Transition Relation 4.2 Conditions for the Transitions 4.3 Illustrative Examples 5 Proving Preservation of Consensus 6 Conclusion References Embedding Approximation in Event-B: Safe Hybrid System Design Using Proof and Refinement 1 Introduction 2 Event-B: A Refinement and Proof State Based Method 3 Hybrid Systems Modelling Features 3.1 A Theory of Continuous Mathematics 3.2 A Theory of Approximation 4 Modelling Hybrid Systems Using Event-B 4.1 Generic Model and Its Refinement 4.2 Proof Obligations 4.3 Instantiation of the Generic Model 5 Our Framework 5.1 Limitations: Exact vs Approximate Refinement 5.2 Approximate Refinement 5.3 Formalising Approximate Refinement in Event-B 5.4 Proof Obligations: Revisited for Approximate Refinement 5.5 Exact Refinement as a Particular Case of Approximate Refinement 6 Case Study 6.1 Problem Statement 6.2 System Requirements 6.3 Refinement Strategy 6.4 Event-B Development 7 Conclusion References Formal Foundations for Intel SGX Data Center Attestation Primitives 1 Introduction 2 Related Work 2.1 Secure Remote Execution 2.2 Formalizations by Intel 2.3 Discussion 3 Proposed Approach 3.1 Symbolic Model 3.2 Adversary Model 3.3 Security Properties 4 Industrial Case Study: Non-QVE Based DCAP 4.1 Symbolic Model Generation 4.2 Formalization and Verification of Properties 5 Conclusion References Short Papers Towards Modeling and Verification of the CKB Block Synchronization Protocol in Coq 1 Introduction 2 Preliminaries 2.1 The Block Synchronization 2.2 The CKB Block Synchronization Protocol 3 Modeling and Verifying the Protocol in Coq 3.1 Connecting Header Stage 3.2 Downloading Block Stage 3.3 Accepting Block Stage 4 Attack Simulation 5 Conclusion and Future Work References Accurate Abstractions for Controller Synthesis with Non-uniform Disturbances 1 Introduction 2 Preliminaries 2.1 Notation 2.2 Systems and Refinement 2.3 Time-Sampled Control Systems 3 Computation of Abstraction 3.1 A Generic Construction 3.2 Growth Bound Computation 3.3 ComputeAbs: Abstraction Algorithm 4 Experimental Results References Formalising Privacy-Preserving Constraints in Microservices Architecture 1 Introduction 2 Privacy Issues in Modern Software Design 3 Background: Event-B and ProB 4 Verification of Privacy-Preserving Constrains in MSA Using Event-B 4.1 Approach Description 4.2 Application of the Approach to the EHR Example 5 Related Work and Conclusions References Algebraic Approach for Confidence Evaluation of Assurance Cases 1 Introduction 2 Related Work 3 Goal Structuring Notation (GSN) 4 Truthmaker Semantics and Confidence 4.1 Truthmakers 4.2 Frame, Interpretation, and Confidence 5 Relation to Probabilistic Evaluation 6 Multi-legged Argument 7 Concrete Example 8 Conclusion and Future Work References Doctoral Symposium Paper Verification of a TLSF Algorithm in Embedded System 1 Background 2 Verification Outline placeholder 2.1 Global Nature 2.2 The Function of Allocate 2.3 The Function of Release 3 Conclusion and Future Work References Author Index