Formal Methods for Industrial Critical Systems: 16th International Workshop, FMICS 2011, Trento, Italy, August 29-30, 2011, Proceedings (Lecture Notes in Computer Science, 6959)

This book constitutes the proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2011, held in Trento, Italy, in August 2011. The 16 papers presented together with 2 invited talks were carefully reviewed and selected from 39 submissions. The aim of the FMICS workshop series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. It also strives to promote research and development for the improvement of formal methods and tools for industrial applications. Front Matter....Pages - Towards Trustworthy Aerospace Systems: An Experience Report....Pages 1-4 Satisfiability at Microsoft....Pages 5-5 Lightweight Verification of a Multi-Task Threaded Server: A Case Study With The Plural Tool....Pages 6-20 Runtime Verification of Typical Requirements for a Space Critical SoC Platform....Pages 21-36 Past Time LTL Runtime Verification for Microcontroller Binary Code....Pages 37-51 A SAT-Based Approach for the Construction of Reusable Control System Components....Pages 52-67 Formal Safety Analysis in Industrial Practice....Pages 68-84 Structural Test Coverage Criteria for Integration Testing of LUSTRE/SCADE Programs....Pages 85-101 Formal Analysis of a Triplex Sensor Voter in an Industrial Context....Pages 102-116 Experiences with Formal Engineering: Model-Based Specification, Implementation and Testing of a Software Bus at Neopost.....Pages 117-133 Symbolic Power Analysis of Cell Libraries....Pages 134-148 An Automated Semantic-Based Approach for Creating Tasks from Matlab Simulink Models....Pages 149-164 Performability Measure Specification: Combining CSRL and MSL....Pages 165-179 Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit Using CADP....Pages 180-195 Transforming SOS Specifications to Linear Processes....Pages 196-211 Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study....Pages 212-227 Hierarchical Modeling and Formal Verification. An Industrial Case Study Using Reo and Vereofy....Pages 228-243 Modeling and Verifying Timed Compensable Workflows and an Application to Health Care....Pages 244-259 Back Matter....Pages -