Symposium on Real-Time and Hybrid Systems: Essays Dedicated to Professor Chaochen Zhou on the Occasion of His 80th Birthday (Lecture Notes in Computer Science (11180))

This volume is published in honor of Professor Chaochen Zhou’s 80th birthday. The Festschrift contains 13 refereed papers by leading researchers who were among the participants of the celebratory conference in Changsha, China that took place in October 2017. The papers cover a broad spectrum of subjects related to Formal Methods for the development of computer systems. Topics include Probabilistic Programming, Concurrency, Quantum Computing, Domain Engineering, Real-time and Hybrid Systems, and Cloud Computing. Chaochen Zhou is internationally recognized for his own contributions and for the wide influence that he has had through his appointments in Oxford (UK) where he collaborated with Professor Tony Hoare, Lyngby (Denmark) where he worked with Professor Dines Bjørner, UNU-IIST (Macau) where he moved from being Principal Research Fellow to his appointed as Director of the Institute, as well as in Beijing. His book on the Duration Calculus (joint with Michael Hansen) made a seminal contribution to specifying and reasoning about real-time systems. Chaochen Zhou’s contributions have been marked by his election as a member of the Chinese Academy of Sciences. Preface 7 Organization 8 Contents 9 Think Sequential, Run Parallel 11 1 Introduction 11 2 From Think Parallel to Think Sequential 12 2.1 Graphs and Graph Partition 12 2.2 Programming Model 13 2.3 Parallel Computation Model 14 2.4 Features of GRAPE 16 3 Programming with GRAPE 18 3.1 Graph Traversal 18 3.2 Graph Simulation 20 3.3 Graph Connectivity 22 3.4 Minimum Spanning Tree 24 4 Experimental Study 27 5 Concluding Remarks 32 References 33 Concurrency: Handling Interference Formally 36 1 Introduction 36 2 Model-Oriented Formal Semantics 38 2.1 SOS of Concurrency 39 2.2 Granularity 40 2.3 Operational Semantics: A Little Context 41 2.4 Denotational Semantics and Interference 42 3 Axiomatic View 43 3.1 Separation Logic 44 3.2 Rely/Guarantee 46 4 Conclusions 48 References 49 Decidability of the Initial-State Opacity of Real-Time Automata 54 1 Introduction 54 2 Preliminaries 55 2.1 Finite-State Automata and Regular Expressions 56 2.2 Real-Time Automata 58 2.3 Initial-State Opacity of Real-Time Automata 59 3 Correspondence Between NFAs and Real-Time Automata 60 4 Decidability 63 4.1 Calculating Time Between Observable Events 63 4.2 Constructing Real-Time Automata Aobs, Aobs,s and Aobs,ns 66 4.3 Building Trace-Equivalent NFAs 68 5 Conclusion 69 References 69 Domain Science and Engineering A Review of 10 Years Work and a Laudatio The ZCC Fest, 20 October 2017, Changsha, China 71 1 Introduction 71 1.1 Recent Papers and Reports 72 1.2 Recent Experiments 72 1.3 My Emphasis on Software Systems 72 1.4 How Did We Get to Domain Science and Engineering? 73 1.5 Preliminaries 73 1.6 The Papers 74 1.7 Structure of This Paper 74 2 Manifest Domains: Analysis & Description BjornerDAADL2018 74 2.1 A Domain Ontology 75 2.2 From Manifest Parts to Domain Behaviours 77 2.3 Contributions of BjornerDAADL2018 – and Open Problems 78 3 Related Papers 78 3.1 Domain Facets: Analysis & Description BjornerFAoCFacets,dines:facs:2008 78 3.2 From Domains to Requirements BjornerFAoC2015Req,dines:ugo65:2008 79 3.3 Formal Models of Processes and Prompts BjornerFAoCProcesses,2013daspsjaist 81 3.4 To Every Manifest Domain Mereology a CSP Expression BjornerMereologyCSP2017 86 4 Domain Science & Engineering: A Philosophy Basis 2018:Bjorner:philo 87 5 The Experiments BjornerUrbanPlanningProcesses2017,Clem84,RSL,RaiseMethod,Kant,Haff87,CCITT81,Hoare85sps2004,lexicon,Oest86,db02spsamorespsmaint,kaisorlander1994,kaisorlander1997,kaisorlander2002,kaisorlander2016,db02spsamorespsros 88 6 Summary 88 7 Laudatio 89 8 Bibliography 90 8.1 Bibliographical Notes 90 References 91 HAT: Analyzing Linear Hybrid Automata as Labelled Transition System 95 1 Introduction 95 2 Notations 97 2.1 Linear Hybrid Automata 97 2.2 Labelled Linear Transition System 98 2.3 LTS Semantic for LHA 99 3 Quantifier-Free LTS Construction for LHA 99 4 Implementation and Experiment 104 4.1 Tool Implementation 104 4.2 Case Studies 106 5 Related Works 110 5.1 Reachability Analysis 110 5.2 Invariant Generation 111 5.3 Termination Analysis 112 5.4 TS Construction for HA 112 6 Conclusion 112 References 113 Overview: System Architecture Virtual Integration based on an AADL Model 115 1 Introduction 115 2 SAVI Virtual Integration for Safety-Critical Systems 117 2.1 Modelling Complex Safety-Critical Systems 118 2.2 Model Transformation-Based Integration 118 2.3 Model Bus-Based Integration 119 3 Non-functional Properties Analysis for SAVI 120 3.1 Safety Analysis 120 3.2 Dynamic Reconfiguration 121 3.3 Reliability Analysis 121 3.4 Schedulability Analysis 122 4 A Tool for Non-functional Properties Analysis 122 5 Challenges 123 6 Conclusions 123 References 124 Characterization and Verification of Stuttering Equivalence 126 1 Introduction 126 2 Stuttering Equivalence and -Bisimulation 127 3 Stuttering Bisimulation with Induction 131 4 Well-Founded Bisimulation 135 5 Related Works 139 6 Conclusion 141 References 141 Q|SI"526930B : A Quantum Programming Environment 143 1 Introduction 143 2 Quantum while-Language 146 3 The Structure of Q|SI"526930B 146 3.1 Basic Features of Q|SI"526930B 147 3.2 Main Components of Q|SI"526930B 148 3.3 Implementation of Q|SI"526930B 149 4 The Quantum Compiler 149 4.1 f-QASM 152 4.2 Decomposition of a General Unitary Transformation 155 5 The Quantum Simulator 156 5.1 Quantum Types 156 6 Experiments 162 7 Conclusions 163 A Setup and Configuration of Q|SI"526930B 164 B Experiment-Qloop Case 164 B.1 Input and Output 164 B.2 Results 165 B.3 Features and Analysis 165 C BB84 Case 166 C.1 Simple BB84 Case 166 C.2 BB84 Case, Multi-client 168 C.3 BB84 Case with Noise 168 D Grover's Search Algorithm 171 D.1 A Simple Grover's Search Algorithm 171 D.2 Multi-object Grover's Search Algorithm 172 References 172 The Demon, the Gambler, and the Engineer 175 1 Introduction 175 2 Related Work 177 3 Traditional Hybrid Automata Models 179 3.1 Running Example 179 3.2 Deterministic Environmental Sensing 181 3.3 Demonic Modelling 183 3.4 Stochastic Modelling 185 4 Bayesian Hybrid Automata 187 5 Summary 194 References 194 Linking Theories of Probabilistic Programming 196 1 Introduction 196 2 Probabilistic Programming Language 197 2.1 Probabilistic Choice 198 2.2 Conditional Choice 199 2.3 Sequential Composition 201 2.4 Total Assignment 201 3 Normal Form Reduction 202 3.1 Finite Normal Form 202 3.2 Infinite Normal Form 206 3.3 Continuity 207 3.4 Recursion 208 4 Testing Programs 211 5 Operational Approach 213 6 Conclusions 219 References 220 Space for Traffic Manoeuvres: An Overview 221 1 Introduction 221 2 Model 223 2.1 Multi-Lane Spatial Logic 225 3 Controller 226 4 Safety 227 5 Linking 228 5.1 Linking: Distance Controller DC 229 5.2 Linking: Lane-Change Controller LPC 230 6 Tool Support 231 6.1 Satisfiability Problem 231 6.2 Search for Tool Support: Positive Results 233 6.3 EMLSL with Modalities 234 6.4 MLSL with Scopes 235 7 Conclusion 236 References 238 Cloud Robotics: A Distributed Computing View 241 Abstract 241 1 Introduction 241 2 From Backend Computer to Cloud 242 3 Cloud Roles 244 3.1 Computation Support 244 3.2 Data Support 245 3.3 Coordination Support 245 4 Challenges to Distributed Computing 246 4.1 QoS-Awarness 247 4.2 Autonomy Promotion 249 4.3 Collective Intelligence 250 4.4 Ecosystem Evolution 251 5 Our Early Experience 252 5.1 MicROS-Cloud Architecture 252 5.2 Initial Results 252 6 Conclusion 254 Acknowledgements 254 References 254 Analyzing Interrupt Handlers via Interprocedural Summaries 256 1 Introduction 256 2 Features of Interrupt Handlers 257 3 Tabulation of Procedure Summaries 258 4 Procedure Summary Based on Partitioning Inputs 262 5 Implementation and Experiments 265 6 Related Work 268 7 Conclusion and Future Work 270 References 270 Author Index 273 Front Matter ....Pages I-XII Think Sequential, Run Parallel (Wenfei Fan, Muyang Liu, Ruiqi Xu, Lei Hou, Dongze Li, Zizhong Meng)....Pages 1-25 Concurrency: Handling Interference Formally (Cliff B. Jones)....Pages 26-43 Decidability of the Initial-State Opacity of Real-Time Automata (Lingtai Wang, Naijun Zhan)....Pages 44-60 Domain Science and Engineering A Review of 10 Years Work and a Laudatio The ZCC Fest, 20 October 2017, Changsha, China (Dines Bjørner)....Pages 61-84 HAT: Analyzing Linear Hybrid Automata as Labelled Transition System (Lei Bu, Hui Jiang, Xin Chen, Enyi Tang, Xuandong Li)....Pages 85-104 Overview: System Architecture Virtual Integration based on an AADL Model (Yunwei Dong, Xiaomin Wei, Mingrui Xiao)....Pages 105-115 Characterization and Verification of Stuttering Equivalence (Xinxin Liu, Wenhui Zhang)....Pages 116-132 \(Q|SI\rangle \) : A Quantum Programming Environment (Shusen Liu, Xin Wang, Li Zhou, Ji Guan, Yinan Li, Yang He et al.)....Pages 133-164 The Demon, the Gambler, and the Engineer (Martin Fränzle, Paul Kröger)....Pages 165-185 Linking Theories of Probabilistic Programming (He Jifeng)....Pages 186-210 Space for Traffic Manoeuvres: An Overview (Ernst-Rüdiger Olderog)....Pages 211-230 Cloud Robotics: A Distributed Computing View (Wang Huaimin, Ding Bo, Jie Xu)....Pages 231-245 Analyzing Interrupt Handlers via Interprocedural Summaries (Xueguang Wu, Liqian Chen, Ji Wang)....Pages 246-262 Back Matter ....Pages 263-263