Verification and Evaluation of Computer and Communication Systems : 11th International Conference, VECoS 2017, Montreal, QC, Canada, August 24{u2013}25, 2017, Proceedings

This book constitutes the proceedings of the 11th International Conference International Conference on Verification and Evaluation of Computer and Communication Systems ( VECoS 2017 ), held at Concordia University, Montreal, Canada, in August 2017. The 13 full papers, together with 3 abstracts in this volume were carefully reviewed and selected from 35 submissions. The aim of the VECoS conference is to bring together researchers and practitioners in the areas of verification, control, performance and dependability evalu-ation in order to discuss state-of-the-art and challenges in modern computer and communication systems in which functional and extra-functional properties are strongly in terrelated. Thus, the main motivation for VECoS is to encourage the cross-fertilization between various formal verification and evaluation approaches, methods and techniques, and especially those developed for concurrent and dis-tributed hardware/software systems. Read more... Abstract: This book constitutes the proceedings of the 11th International Conference International Conference on Verification and Evaluation of Computer and Communication Systems ( VECoS 2017 ), held at Concordia University, Montreal, Canada, in August 2017. The 13 full papers, together with 3 abstracts in this volume were carefully reviewed and selected from 35 submissions. The aim of the VECoS conference is to bring together researchers and practitioners in the areas of verification, control, performance and dependability evalu-ation in order to discuss state-of-the-art and challenges in modern computer and communication systems in which functional and extra-functional properties are strongly in terrelated. Thus, the main motivation for VECoS is to encourage the cross-fertilization between various formal verification and evaluation approaches, methods and techniques, and especially those developed for concurrent and dis-tributed hardware/software systems Preface 6 Organization 7 Keynote Speakers 9 Live Run-Time Verification of Parallel Heterogeneous Real-Time Systems 10 Measuring and Enhancing Smart Grid Security 11 Deadlock Analysis and Control of Resource Allocation Systems: Structural and Reachability Graph Approaches 12 Contents 13 Formal Probabilistic Analysis of a Virtual Fixture Control Algorithm for a Surgical Robot 15 1 Introduction 15 2 Related Work 16 3 Preliminaries 17 3.1 Probabilistic Model Checking and PRISM 17 3.2 Virtual Fixture Control Algorithm for Surgical Robots 18 4 Formalization of the Virtual Fixture Algorithm Using the PRISM Language 19 4.1 Force Module 20 4.2 Velocity Module 21 4.3 Position Module 21 4.4 Multiple Surgical Tools 22 5 Virtual Fixture Control Algorithm 22 5.1 Deadlock Freedom 22 5.2 Reachability 23 5.3 Out-of-Boundary 24 5.4 Collision Freeness 26 6 Testing on Al-Zahrawi 27 7 Conclusions 29 References 29 Performance Analysis of Multi-services Call Admission Control in Cellular Network Using Probabilistic Model Checking 31 1 Introduction 31 2 Probabilistic Model Checking 33 2.1 Labelled CTMC 33 2.2 Temporal Logic CSL 33 3 Formal Modelling of CAC Schemes 34 3.1 Basic CAC (B-CAC) Schema 36 3.2 Queuing CAC (Q-CAC) Schema 37 3.3 Real Time Priority CAC (RTP-CAC) Schema 38 3.4 Real Time Priority and Queuing (RTPQ-CAC) Schema 40 4 Formal Specification of Performance Properties by CSL Formulas 41 4.1 Checking Steady-State Formulas 41 4.2 Checking Transient Formulas 42 4.3 Checking Reward Formulas 43 5 Model Checking Results of CSL Formulas 43 6 Conclusion 45 References 46 Application of Generalized Stochastic Petri Nets to Performance Modeling of the RF Communication in Sensor Networks 47 1 Introduction 47 2 The Basic Models 49 3 An Overview of Generalized Stochastic Petri Nets 49 4 GSPN Models of the RF Transmission in Wireless Sensor Networks 50 5 Performance Measures 53 6 Numerical Results 55 7 Conclusion 60 References 60 Regression-Based Statistical Bounds on Software Execution Time 62 1 Introduction 62 2 Common Probabilistic Techniques 64 2.1 Probabilistic Measurement-Based Timing Analysis 64 2.2 Linear Regression in the Nutshell 65 3 Linear Regression for MET 66 3.1 The Maximal Regression Model 66 3.2 Identifying the Predictors: Stepwise Regression 68 3.3 Quality of Input Data: Cook's Distance 69 4 A Design Flow for MET 69 4.1 Instrumentation and Measurements 69 4.2 Final Flow Steps 71 5 A JPEG Decoder on a SPARC Platform 71 5.1 Instrumentation and Measurements 72 5.2 Predictors Identification and Model Construction 72 6 Related Work 75 7 Conclusions 76 References 77 WCET Analysis by Model Checking for a Processor with Dynamic Branch Prediction 78 1 Introduction 78 2 Background and Related Works 79 2.1 Branch Prediction Basis 79 2.2 Analysis of Branch Prediction Techniques 80 2.3 Model Checking and WCET Analysis of Processors 81 3 Description of the Target Microarchitecture 81 3.1 Memory Hierarchy 81 3.2 Execution Pipeline and Instruction Prefetch Buffer 82 3.3 Branch Prediction 82 3.4 Analyzability and Predictability 83 4 Our WCET Analysis Framework 83 5 Models 85 5.1 Modeling the Program 85 5.2 Modeling the Pipeline 86 5.3 Modeling the Memory Hierarchy 87 6 Experimental Results 88 7 Conclusion 91 References 91 Factor-Based C-AMAT Analysis for Memory Optimization 93 1 Introduction 93 2 FC-AMAT Analysis Model 95 3 Methodology 98 4 Results 99 4.1 Basic L1 Cache Configurations 100 4.2 Basic L2 Cache Configuration 102 4.3 Advanced Cache Configurations 103 5 Related Work 104 6 Conclusion 104 References 105 An Experimental Comparison of Two Approaches for Diagnosability Analysis of Discrete Event Systems - A Railway Case-Study 106 1 Introduction 106 2 Preliminaries 107 2.1 The System Model 107 2.2 Definition of Diagnosability 108 3 The Considered Approaches 109 3.1 The Diagnoser-based Approach 109 3.2 The Model-Checking Reformulation Approach 113 3.3 The Main Features of the Considered Approaches 115 4 The Railway Case-Study 116 4.1 Railway Level Crossing Benchmark 117 4.2 Experimentation 118 5 Conclusion 120 References 120 Mobility Load Balancing over Intra-frequency Heterogeneous Networks Using Handover Adaptation 122 1 Introduction 122 2 Literature Review of MLB in HetNets 124 2.1 MLB in Idle Mode: Load-Aware User Association 124 2.2 MLB in Connected Mode 125 3 Problem Formulation and System Model 126 4 MLB Based HO Biasing 128 5 Simulation Assumptions and Results 130 6 Conclusion 135 References 135 A Toolset for Mobile Systems Testing 138 1 Introduction 138 2 Toolset Overview 140 3 Scenario Specification 141 3.1 Scenario Modeling 142 3.2 Scenario Format Checks 144 3.3 Scenarios Processing 145 4 Trace Analysis 145 4.1 Principles 146 4.2 Verdict Analysis 147 5 Results 148 6 Related Works 150 7 Conclusion 150 References 151 Intertwined Global Optimization Based Reachability Analysis 153 1 Introduction 153 2 Preliminaries 154 2.1 Hybrid System Modeling: System of Stochastic Recurrence Equations 155 2.2 Latin Hypercube Sampling 156 2.3 Hypothesis Testing 157 3 Proposed Methodology 159 3.1 Forward-Backward Reachability Analysis 160 4 Application: PLL Frequency Synthesizer 162 5 Conclusion 166 References 167 Analyzing Distributed Pi-Calculus Systems by Using the Rewriting Engine Maude 169 1 Introduction 169 2 Distributed Pi-Calculus 170 2.1 Bisimulations for Distributed Systems with Migration 174 3 Translating Distributed Pi-Calculus into Maude 175 4 Analyzing Distributed Systems by Using Maude 180 5 Conclusion and Related Work 182 References 183 TT-BIP: Using Correct-by-Design BIP Approach for Modelling Real-Time System with Time-Triggered Paradigm 185 1 Introduction 185 2 The BIP Framework 186 3 Problem Statement and the Proposed Solution 188 4 Transformation of a BIP Model into a TT-BIP Model 191 4.1 Analysis Phase 192 4.2 Transformation of Task Components 192 4.3 Expressing Timing Constraints and Time Progress Conditions over a Common Global Clock 193 4.4 Building TTCC Components 195 4.5 Conflict Resolution Protocol Component 197 4.6 Cross-Layer Interactions 198 5 Implemantation and Use Case 199 6 Conclusion 200 References 201 Uppaal vs Event-B for Modelling Optimised Link State Routing 203 1 Introduction 203 2 Formal Methods, Model Checking, and Theorem Proving 205 2.1 Model Checking--Uppaal's Timed Automata 205 2.2 Theorem Proving--Event-B 206 3 An Overview of Optimised Link State Routing 207 4 Formal Modelling of the OLSR 207 4.1 Uppaal Model of the OLSR 207 4.2 Event-B Model of the OLSR 209 5 Comparison 211 5.1 Uppaal Model vs Event-B Model 211 5.2 Uppaal vs Event-B 213 6 Conclusions and Usage Guidelines 215 References 216 Author Index 218 Front Matter ....Pages I-XVI Formal Probabilistic Analysis of a Virtual Fixture Control Algorithm for a Surgical Robot (Muhammad Saad Ayub, Osman Hasan)....Pages 1-16 Performance Analysis of Multi-services Call Admission Control in Cellular Network Using Probabilistic Model Checking (Sana Younes, Momtez Benmbarek)....Pages 17-32 Application of Generalized Stochastic Petri Nets to Performance Modeling of the RF Communication in Sensor Networks (Sedda Hakmi, Ouiza Lekadir, Djamil Aïssani)....Pages 33-47 Regression-Based Statistical Bounds on Software Execution Time (Peter Poplavko, Ayoub Nouri, Lefteris Angelis, Alexandros Zerzelidis, Saddek Bensalem, Panagiotis Katsaros)....Pages 48-63 WCET Analysis by Model Checking for a Processor with Dynamic Branch Prediction (Armel Mangean, Jean-Luc Béchennec, Mikaël Briday, Sébastien Faucou)....Pages 64-78 Factor-Based C-AMAT Analysis for Memory Optimization (Qi Yu, Libo Huang, Cheng Qian, Jianqiao Ma, Zhiying Wang)....Pages 79-91 An Experimental Comparison of Two Approaches for Diagnosability Analysis of Discrete Event Systems - A Railway Case-Study (Abderraouf Boussif, Mohamed Ghazel)....Pages 92-107 Mobility Load Balancing over Intra-frequency Heterogeneous Networks Using Handover Adaptation (Hana Jouini, Mohamed Escheikh, Kamel Barkaoui, Tahar Ezzedine)....Pages 108-123 A Toolset for Mobile Systems Testing (Pierre André, Nicolas Rivière, Hélène Waeselynck)....Pages 124-138 Intertwined Global Optimization Based Reachability Analysis (Ibtissem Seghaier, Sofiène Tahar)....Pages 139-154 Analyzing Distributed Pi-Calculus Systems by Using the Rewriting Engine Maude (Bogdan Aman, Gabriel Ciobanu)....Pages 155-170 TT-BIP: Using Correct-by-Design BIP Approach for Modelling Real-Time System with Time-Triggered Paradigm (Hela Guesmi, Belgacem Ben Hedia, Simon Bliudze, Saddek Bensalem, Briag Le Nabec)....Pages 171-188 Uppaal vs Event-B for Modelling Optimised Link State Routing (Mojgan Kamali, Luigia Petre)....Pages 189-203 Back Matter ....Pages 205-205 This book constitutes the proceedings of the 11th International Conference International Conference on Veri{uFB01}cation and Evaluation of Computer and Communication Systems ( VECoS 2017 ), held at Concordia University, Montreal, Canada, in August 2017. The 13 full papers, together with 3 abstracts in this volume were carefully reviewed and selected from 35 submissions. The aim of the VECoS conference is to bring together researchers and practitioners in the areas of veri{uFB01}cation, control, performance and dependability evalu-ation in order to discuss state-of-the-art and challenges in modern computer and communication systems in which functional and extra-functional properties are strongly in terrelated. Thus, the main motivation for VECoS is to encourage the cross-fertilization between various formal veri{uFB01}cation and evaluation approaches, methods and techniques, and especially those developed for concurrent and dis-tributed hardware/software systems