Formal Methods and Software Engineering

1. Front Matter

   Pages I-XVII

   PDF

2. A (Proto) Logical Basis for the Notion of a Structured Argument in a Safety Case

   • Valentín Cassano, Thomas S. E. Maibaum, Silviya Grigorova

   Pages 1-17

3. Promotion of Formal Approaches in Japanese Software Industry and a Best Practice of FeliCa’s Case (Extended Abstract)

   • Keijiro Araki, Taro Kurita

   Pages 18-25

4. Automated Requirements Validation for ATP Software via Specification Review and Testing

   • Weikai Miao, Geguang Pu, Yinbo Yao, Ting Su, Danzhu Bao, Yang Liu et al.

   Pages 26-40

5. Automatic Generation of Potentially Pathological Instances for Validating Alloy Models

   • Takaya Saeki, Fuyuki Ishikawa, Shinichi Honiden

   Pages 41-56

6. A General Lattice Model for Merging Symbolic Execution Branches

   • Dominic Scheurer, Reiner Hähnle, Richard Bubel

   Pages 57-73

7. A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid Automata

   • Ryo Yanase, Tatsunori Sakai, Makoto Sakai, Satoshi Yamane

   Pages 74-89

8. Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks

   • Richard Banach, Michael Butler

   Pages 90-105

9. A System Substitution Mechanism for Hybrid Systems in Event-B

   • Guillaume Babin, Yamine Aït-Ameur, Neeraj Kumar Singh, Marc Pantel

   Pages 106-121

10. Service Adaptation with Probabilistic Partial Models

    • Manman Chen, Tian Huat Tan, Jun Sun, Jingyi Wang, Yang Liu, Jing Sun et al.

    Pages 122-140

11. A Formal Approach to Identifying Security Vulnerabilities in Telecommunication Networks

    • Linas Laibinis, Elena Troubitsyna, Inna Pereverzeva, Ian Oliver, Silke Holtmanns

    Pages 141-158

12. Multi-threaded On-the-Fly Model Generation of Malware with Hash Compaction

    • Nguyen Minh Hai, Quan Thanh Tho, Le Duc Anh

    Pages 159-174

13. CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions

    • Marco Rocchetto, Nils Ole Tippenhauer

    Pages 175-192

14. Towards the Formal Verification of Data-Intensive Applications Through Metric Temporal Logic

    • Francesco Marconi, Marcello M. Bersani, Madalina Erascu, Matteo Rossi

    Pages 193-209

15. Proving Event-B Models with Reusable Generic Lemmas

    • Alexei Iliasov, Paulius Stankaitis, Alexander Romanovsky

    Pages 210-225

16. Formal Availability Analysis Using Theorem Proving

    • Waqar Ahmad, Osman Hasan

    Pages 226-242

17. Formal Verification of the rank Algorithm for Succinct Data Structures

    • Akira Tanaka, Reynald Affeldt, Jacques Garrigue

    Pages 243-260

18. Contextual Trace Refinement for Concurrent Objects: Safety and Progress

    • Brijesh Dongol, Lindsay Groves

    Pages 261-278

19. Local Livelock Analysis of Component-Based Models

    • Madiel S. Conserva Filho, Marcel Vinicius Medeiros Oliveira, Augusto Sampaio, Ana Cavalcanti

    Pages 279-295

20. Session-Based Compositional Analysis for Actor-Based Languages Using Futures

    • Eduard Kamburjan, Crystal Chang Din, Tzu-Chun Chen

    Pages 296-312

This book constitutes the refereed proceedings of the 18th International Conference on Formal Engineering Methods, ICFEM 2016, held in Tokyo, Japan, in November 2016. The 27 revised full papers presented together with three invited talks were carefully reviewed and selected from 64 submissions. The conference focuses in all areas related to formal engineering meth-ods, such as verification and validation, software engineering, formal specification and modeling, software security, and software reliability.

• cloud computing
• distributed systems
• formal methods
• model checking
• self-adaptive systems

• School of Information Science, Japan Advanced Institute of Science and Technology (JAIST), Nomi, Japan

  Kazuhiro Ogata

• Department of Computing and Software, McMaster University, Hamilton, Canada

  Mark Lawford

• Department of Computer Science, Hosei University, Tokyo, Japan

  Shaoying Liu

Policies and ethics