Formal Methods and Software Engineering: 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings

✍ Scribed by Kazuhiro Ogata, Mark Lawford, Shaoying Liu (eds.)

• Publisher: Springer International Publishing
• Year: 2016
• Tongue: English
• Leaves: 502
• Series: Lecture Notes in Computer Science 10009
• Edition: 1
• Category: Library

✦ Synopsis

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.

✦ Table of Contents

Front Matter....Pages I-XVII
A (Proto) Logical Basis for the Notion of a Structured Argument in a Safety Case....Pages 1-17
Promotion of Formal Approaches in Japanese Software Industry and a Best Practice of FeliCa’s Case (Extended Abstract)....Pages 18-25
Automated Requirements Validation for ATP Software via Specification Review and Testing....Pages 26-40
Automatic Generation of Potentially Pathological Instances for Validating Alloy Models....Pages 41-56
A General Lattice Model for Merging Symbolic Execution Branches....Pages 57-73
A Case Study of Formal Approach to Dynamically Reconfigurable Systems by Using Dynamic Linear Hybrid Automata....Pages 74-89
Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks....Pages 90-105
A System Substitution Mechanism for Hybrid Systems in Event-B....Pages 106-121
Service Adaptation with Probabilistic Partial Models....Pages 122-140
A Formal Approach to Identifying Security Vulnerabilities in Telecommunication Networks....Pages 141-158
Multi-threaded On-the-Fly Model Generation of Malware with Hash Compaction....Pages 159-174
CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions....Pages 175-192
Towards the Formal Verification of Data-Intensive Applications Through Metric Temporal Logic....Pages 193-209
Proving Event-B Models with Reusable Generic Lemmas....Pages 210-225
Formal Availability Analysis Using Theorem Proving....Pages 226-242
Formal Verification of the rank Algorithm for Succinct Data Structures....Pages 243-260
Contextual Trace Refinement for Concurrent Objects: Safety and Progress....Pages 261-278
Local Livelock Analysis of Component-Based Models....Pages 279-295
Session-Based Compositional Analysis for Actor-Based Languages Using Futures....Pages 296-312
An Event-B Development Process for the Distributed BIP Framework....Pages 313-328
Partial Order Reduction for State/Event Systems....Pages 329-345
Concolic Unbounded-Thread Reachability via Loop Summaries....Pages 346-362
Scaling BDD-based Timed Verification with Simulation Reduction....Pages 363-382
Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots....Pages 383-399
Decision Problems for Parametric Timed Automata....Pages 400-416
Verifying Nested Lock Priority Inheritance in RTEMS with Java Pathfinder....Pages 417-432
An SMT-Based Approach to the Formal Analysis of MARTE/CCSL....Pages 433-449
Checking SysML Models for Co-simulation....Pages 450-465
A CEGAR Scheme for Information Flow Analysis....Pages 466-483
Back Matter....Pages 485-486

✦ Subjects

Software Engineering;Programming Techniques;Programming Languages, Compilers, Interpreters;Logics and Meanings of Programs;Mathematical Logic and Formal Languages;Computer Communication Networks