Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings

Description

This book constitutes the proceedings of the Third International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2017, held in Changsha, China, in October2017.The 19 full papers presented together with 3 invited talks were carefully reviewed and selected from 31 submissions. The aim of the symposium is to bring together international researchers and practitioners in the field of software technology. Its focus is on probabilistic and statistical analysis; timed and hybrid systems; program analysis; modeling and verification; formalization; and tools. Front Matter ....Pages I-XVIII Front Matter ....Pages 1-1 General Lessons from a Rely/Guarantee Development (Cliff B. Jones, Andrius Velykis, Nisansala Yatapanage)....Pages 3-22 Front Matter ....Pages 23-23 Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs (Vahid Hashemi, Andrea Turrini, Ernst Moritz Hahn, Holger Hermanns, Khaled Elbassioni)....Pages 25-41 Better Automated Importance Splitting for Transient Rare Events (Carlos E. Budde, Pedro R. D’Argenio, Arnd Hartmanns)....Pages 42-58 On the Criticality of Probabilistic Worst-Case Execution Time Models (Luca Santinelli, Zhishan Guo)....Pages 59-74 Front Matter ....Pages 75-75 Nested Timed Automata with Invariants (Yuwei Wang, Guoqiang Li, Shoji Yuen)....Pages 77-93 Multi-core Cyclic Executives for Safety-Critical Systems (Calvin Deutschbein, Tom Fleming, Alan Burns, Sanjoy Baruah)....Pages 94-109 Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus (Dimitar P. Guelev, Shuling Wang, Naijun Zhan)....Pages 110-127 Front Matter ....Pages 129-129 Termination of Semi-algebraic Loop Programs (Yi Li)....Pages 131-146 Computing Exact Loop Bounds for Bounded Program Verification (Tianhai Liu, Shmuel Tyszberowicz, Bernhard Beckert, Mana Taghdiri)....Pages 147-163 AndroidLeaker: A Hybrid Checker for Collusive Leak in Android Applications (Zipeng Zhang, Xinyu Feng)....Pages 164-180 Front Matter ....Pages 181-181 Remark on Some \(\pi \) Variants (Jianxin Xue, Huan Long, Yuxi Fu)....Pages 183-199 Reasoning About Periodicity on Infinite Words (Wanwei Liu, Fu Song, Ge Zhou)....Pages 200-215 On Equivalence Checking of Nondeterministic Finite Automata (Chen Fu, Yuxin Deng, David N. Jansen, Lijun Zhang)....Pages 216-231 A New Decomposition Method for Attractor Detection in Large Synchronous Boolean Networks (Andrzej Mizera, Jun Pang, Hongyang Qu, Qixia Yuan)....Pages 232-249 Construction of Abstract State Graphs for Understanding Event-B Models (Daichi Morita, Fuyuki Ishikawa, Shinichi Honiden)....Pages 250-265 A Framework for Modeling and Verifying IoT Communication Protocols (Maithily Diwan, Meenakshi D’Souza)....Pages 266-280 Front Matter ....Pages 281-281 Formal Analysis of Information Flow in HOL (Ghassen Helali, Sofiène Tahar, Osman Hasan, Tsvetan Dunchev)....Pages 283-299 Formalizing SPARCv8 Instruction Set Architecture in Coq (Jiawei Wang, Ming Fu, Lei Qiao, Xinyu Feng)....Pages 300-316 Front Matter ....Pages 317-317 How to Efficiently Build a Front-End Tool for UPPAAL: A Model-Driven Approach (Stefano Schivo, Buğra M. Yildiz, Enno Ruijters, Christopher Gerking, Rajesh Kumar, Stefan Dziwok et al.)....Pages 319-336 PranCS: A Protocol and Discrete Controller Synthesis Tool (Idress Husien, Sven Schewe, Nicolas Berthier)....Pages 337-349 Back Matter ....Pages 351-351