Formal methods for industrial critical systems : 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 : proceedings

This book constitutes the proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015, Oslo, Norway, in June 2015. The 12 papers presented in this volume were carefully reviewed and selected from 20 submissions. They are organized in topical sections: applications; protocols; specification and analysis; verification. Front Matter....Pages 1-14 Formal Verification of Industrial Critical Software....Pages 1-11 Front Matter....Pages 13-13 A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C....Pages 15-30 Intra-procedural Optimization of the Numerical Accuracy of Programs....Pages 31-46 Formal Analysis and Testing of Real-Time Automotive Systems Using UPPAAL Tools....Pages 47-61 Successful Use of Incremental BMC in the Automotive Industry....Pages 62-77 Front Matter....Pages 79-79 Colored Petri Net Modeling of the Publish/Subscribe Paradigm in the Context of Web Services Resources....Pages 81-95 Model Checking a Server-Side Micro Payment Protocol....Pages 96-110 Front Matter....Pages 111-111 Require, Test and Trace IT....Pages 113-127 Applying Finite State Process Algebra to Formally Specify a Computational Model of Security Requirements in the Key2phone-Mobile Access Solution....Pages 128-145 Timed Mobility and Timed Communication for Critical Systems....Pages 146-161 On the Formal Analysis of Photonic Signal Processing Systems....Pages 162-177 Front Matter....Pages 179-179 Automated Verification of Nested DFS....Pages 181-197 On the Formal Verification of Optical Quantum Gates in HOL....Pages 198-211 Back Matter....Pages 213-213