Dependable Software Engineering. Theories, Tools, And Applications: 5th International Symposium, Setta 2019, Shanghai, China, November 27-29, 2019, Proceedings (lecture Notes In Computer Science)

This book constitutes the proceedings of the 5th International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2019, held in Shanghai, China, in November 2019. The 8 full papers presented were carefully reviewed and selected from 26 submissions. They present cutting-edge advancements in the field of formal methods and its interoperability with software engineering and focus on the application of formal techniques and tools for building reliable, safe, secure, and smart systems with multi-dimensional complexities. -- Preface 6 Organization 7 Abstracts 9 The Rise of Model Counting: A Child of SAT Revolution 10 Building and Updating Safety-Critical Embedded Systems with Deterministic Timing and Functional Behaviours 11 Contents 12 A Bounded Model Checking Technique for Higher-Order Programs 13 1 Introduction 13 2 The Language: HORef 16 3 A Bounded Translation for HORef 18 4 A Points-To Analysis for Names 24 5 Implementation and Experiments 26 References 29 Fault Trees from Data: Efficient Learning with an Evolutionary Algorithm 31 1 Introduction 31 2 Related Work 33 3 Background 35 4 Learning Fault Trees with Nature-Inspired Stochastic Optimization 37 4.1 Initialization 38 4.2 Mutation and Recombination 38 4.3 Evaluation 39 4.4 Selection 40 4.5 Termination 40 5 Learning of Partial Fault Trees 40 5.1 Initialization 41 5.2 Mutation and Recombination 41 6 Experimental Evaluation 42 6.1 Experimental Set Up 42 6.2 Synthetic Dataset: Accuracy and Runtime 43 6.3 Synthetic Dataset: Other Statistics 44 6.4 Case Study with Industrial Dataset 45 6.5 Fault Tree Benchmark 45 7 Discussion 45 8 Conclusion and Future Work 47 References 47 Simplifying the Analysis of Software Design Variants with a Colorful Alloy 50 1 Introduction 50 2 Overview 52 3 Language 55 4 Analysis 59 5 Evaluation 61 5.1 Evaluation Subjects 62 5.2 Results 64 6 Related Work 64 7 Conclusion and Future Work 65 References 66 Response Time Analysis of Typed DAG Tasks for G-FP Scheduling 68 1 Introduction 68 2 Related Work 69 3 Preliminaries 70 4 Rationale 71 4.1 Bounding Intra-interference 72 5 Bounding Inter-interference 72 5.1 Bounding Carry-In Interference 73 5.2 Bounding Carry-Out Interference 74 6 Schedulability Analysis 78 7 Evaluation 79 8 Conclusion 81 References 81 A Formal Modeling and Verification Framework for Flash Translation Layer Algorithms 84 1 Introduction 84 2 Informal Development 86 2.1 Modeling FTL Algorithms 86 2.2 Correctness Requirement of FTL Algorithms 87 2.3 Our Proof Technique Based on Invariant 87 3 Modeling FTL and Its Functional Correctness 88 3.1 Disk Device 88 3.2 Flash Device and FTL 89 3.3 The Correctness Definition of FTL 90 4 Verification Framework 90 5 Case Study: Verifying an FTL Algorithm BAST 93 5.1 Overview of BAST 93 5.2 The Global Invariant for BAST 95 5.3 Mechanized Proof and Experience 97 6 Related Work and Conclusion 98 7 Conclusion 99 References 99 Mixed Criticality Scheduling of Probabilistic Real-Time Systems 101 1 Introduction 101 1.1 Problem Discussion and Contribution 103 2 Notations and Definitions 104 2.1 Computational Model 105 3 Probabilistic Scheduling Model 107 3.1 Graph Model 107 3.2 Scheduling Tree 108 4 Evaluation 110 5 Conclusion 116 References 116 Improving the Analysis of GPC in Real-Time Calculus 118 1 Introduction 118 2 RTC Basics 119 2.1 Arrival and Service Curves 119 2.2 Greedy Processing Component (GPC) 120 3 Revised Proof of Output Curves 122 4 Improving Output Arrival Curves 126 5 Experiments 128 5.1 Parameter Setting I 128 5.2 Parameter Setting II 129 6 Conclusion 130 References 132 A Verified Specification of TLSF Memory Management Allocator Using State Monads 134 1 Introduction 134 2 Background and Related Work 136 2.1 TLSF Algorithm 136 2.2 Related Work 137 3 The Data Structure and Configuration 138 3.1 System Configuration 138 3.2 System State 139 3.3 Bitmap Matrix 140 4 Formalizing the Abstract Specification 141 4.1 Invariants 141 4.2 Specification of Allocation 143 4.3 Specification of Deallocation 143 5 Formalizing the Algorithm 144 5.1 State Monads 144 5.2 Formal Specification of Memory Functions 144 6 Formal Verification and Results 147 6.1 Verification Using State Monad 147 6.2 Evaluation 148 7 Conclusion 148 References 149 Author Index 151 Front Matter ....Pages i-xiii A Bounded Model Checking Technique for Higher-Order Programs (Yu-Yang Lin, Nikos Tzevelekos)....Pages 1-18 Fault Trees from Data: Efficient Learning with an Evolutionary Algorithm (Alexis Linard, Doina Bucur, Mariëlle Stoelinga)....Pages 19-37 Simplifying the Analysis of Software Design Variants with a Colorful Alloy (Chong Liu, Nuno Macedo, Alcino Cunha)....Pages 38-55 Response Time Analysis of Typed DAG Tasks for G-FP Scheduling (Xuemei Peng, Meiling Han, Qingxu Deng)....Pages 56-71 A Formal Modeling and Verification Framework for Flash Translation Layer Algorithms (Lei Qiao, Shaofeng Li, Hua Yang, Mengfei Yang)....Pages 72-88 Mixed Criticality Scheduling of Probabilistic Real-Time Systems (Jasdeep Singh, Luca Santinelli, Federico Reghenzani, Konstantinos Bletsas, David Doose, Zhishan Guo)....Pages 89-105 Improving the Analysis of GPC in Real-Time Calculus (Yue Tang, Yuming Jiang, Nan Guan)....Pages 106-121 A Verified Specification of TLSF Memory Management Allocator Using State Monads (Yu Zhang, Yongwang Zhao, David Sanan, Lei Qiao, Jinkun Zhang)....Pages 122-138 Back Matter ....Pages 139-139