Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi’an, China, November 13-17, 2017, Proceedings

Description

This book constitutes the refereed proceedings of the 19th International Conference on Formal Engineering Methods, ICFEM 2017, held in Xi'an, China, in November 2017. The 28 revised full papers presented together with one invited talk and two abstracts of invited talks were carefully reviewed and selected from 80 submissions. The conference focuses on all areas related to formal engineering methods, such as verification and validation, software engineering, formal specification and modeling, software security, and software reliability. Front Matter ....Pages I-XVII Front Matter ....Pages 1-1 Towards Customizable CPS: Composability, Efficiency and Predictability (Wang Yi)....Pages 3-15 Front Matter ....Pages 17-17 Modularization of Refinement Steps for Agile Formal Methods (Fabian Benduhn, Thomas Thüm, Ina Schaefer, Gunter Saake)....Pages 19-35 Model Checking Pushdown Epistemic Game Structures (Taolue Chen, Fu Song, Zhilin Wu)....Pages 36-53 Transforming Timing Requirements into CCSL Constraints to Verify Cyber-Physical Systems (Xiaohong Chen, Ling Yin, Yijun Yu, Zhi Jin)....Pages 54-70 A Framework for Multi-view Reconciliation and for Medical Devices Personalization (Yihai Chen, Bofang Zhang, Ridha Khedri, Huaikou Miao)....Pages 71-87 Compiling Parameterized X86-TSO Concurrent Programs to Cubicle-\(\mathcal {W}\) (Sylvain Conchon, David Declerck, Fatiha Zaïdi)....Pages 88-104 Improving the Scalability of Automatic Linearizability Checking in SPIN (Patrick Doolan, Graeme Smith, Chenyi Zhang, Padmanabhan Krishnan)....Pages 105-121 Verifying Temporal Properties of C Programs via Lazy Abstraction (Zhao Duan, Cong Tian, Zhenhua Duan)....Pages 122-139 Combining Event-B and CSP: An Institution Theoretic Approach to Interoperability (Marie Farrell, Rosemary Monahan, James F. Power)....Pages 140-156 Refinement-Based Modelling and Verification of Design Patterns for Self-adaptive Systems (Thomas Göthel, Nils Jähnig, Simon Seif)....Pages 157-173 Assertion Generation Through Active Learning (Long H. Pham, Ly Ly Tran Thi, Jun Sun)....Pages 174-191 Detecting Energy Bugs in Android Apps Using Static Analysis (Hao Jiang, Hongli Yang, Shengchao Qin, Zhendong Su, Jian Zhang, Jun Yan)....Pages 192-208 A Flexible Approach for Finding Optimal Paths with Minimal Conflicts (Juliana K. F. Bowles, Marco B. Caminati)....Pages 209-225 A Certified Decision Procedure for Tree Shares (Xuan-Bach Le, Thanh-Toan Nguyen, Wei-Ngan Chin, Aquinas Hobor)....Pages 226-242 Classification-Based Parameter Synthesis for Parametric Timed Automata (Jiaying Li, Jun Sun, Bo Gao, Étienne André)....Pages 243-261 A Verification Framework for Stateful Security Protocols (Li Li, Naipeng Dong, Jun Pang, Jun Sun, Guangdong Bai, Yang Liu et al.)....Pages 262-280 A Sliding-Window Algorithm for On-The-Fly Interprocedural Program Analysis (Xin Li, Mizuhito Ogawa)....Pages 281-297 Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking (Si Liu, Peter Csaba Ölveczky, Jatin Ganhotra, Indranil Gupta, José Meseguer)....Pages 298-314 An Improved Android Collusion Attack Detection Method Based on Program Slicing (Yunhao Liu, Xiaohong Li, Zhiyong Feng, Jianye Hao)....Pages 315-331 Parameterized Complexity of Resilience Decision for Database Debugging (Dongjing Miao, Zhipeng Cai)....Pages 332-344 Formal Analysis of Linear Control Systems Using Theorem Proving (Adnan Rashid, Osman Hasan)....Pages 345-361 Policy Dependent and Independent Information Flow Analyses (Manuel Töws, Heike Wehrheim)....Pages 362-378 Improving Probability Estimation Through Active Probabilistic Model Learning (Jingyi Wang, Xiaohong Chen, Jun Sun, Shengchao Qin)....Pages 379-395 Nested Timed Automata with Diagonal Constraints (Yuwei Wang, Yunqing Wen, Guoqiang Li, Shoji Yuen)....Pages 396-412 Integration of Metamorphic Testing with Program Repair Methods Based on Adaptive Search Strategies and Program Equivalence (Tingting Wu, Yunwei Dong, Tsong Yueh Chen, Mingyue Jiang, Man Lau, Fei-Ching Kuo et al.)....Pages 413-429 Learning Types for Binaries (Zhiwu Xu, Cheng Wen, Shengchao Qin)....Pages 430-446 Inconsistency Analysis of Time-Based Security Policy and Firewall Policy (Yi Yin, Yuichiro Tateiwa, Yun Wang, Yoshiaki Katayama, Naohisa Takahashi)....Pages 447-463 An Algebraic Approach to Automatic Reasoning for NetKAT Based on Its Operational Semantics (Yuxin Deng, Min Zhang, Guoqing Lei)....Pages 464-480 Pareto Optimal Reachability Analysis for Simple Priced Timed Automata (Zhengkui Zhang, Brian Nielsen, Kim Guldstrand Larsen, Gilles Nies, Marvin Stenger, Holger Hermanns)....Pages 481-495 Back Matter ....Pages 497-498