Formal Methods for Industrial Critical Systems

1. Front Matter

   PDF

2. Real-Time Specification Patterns and Tools

   • Nouha Abid, Silvano Dal Zilio, Didier Le Botlan

   Pages 1-15

3. Automated Extraction of Abstract Behavioural Models from JMS Applications

   • Elvira Albert, Bjarte M. Østvold, José Miguel Rojas

   Pages 16-31

4. Certifying and Reasoning on Cost Annotations in C Programs

   • Nicolas Ayache, Roberto M. Amadio, Yann Régis-Gianas

   Pages 32-46

5. Waiting for Locks: How Long Does It Usually Take?

   • Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz et al.

   Pages 47-62

6. Microcontroller Assembly Synthesis from Timed Automaton Task Specifications

   • Victor Bandur, Wolfram Kahl, Alan Wassyng

   Pages 63-77

7. Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs

   • Jiri Barnat, Jan Beran, Lubos Brim, Tomas Kratochvíla, Petr Ročkai

   Pages 78-92

8. Range Analysis of Binaries with Minimal Effort

   • Edd Barrett, Andy King

   Pages 93-107

9. Combining Analyses for C Program Verification

   • Loïc Correnson, Julien Signoles

   Pages 108-130

10. Model Checking the FlexRay Startup Phase

    • Sjoerd Cranen

    Pages 131-145

11. Model-Based Risk Assessment Supporting Development of HSE Plans for Safe Offshore Operations

    • Rainer Droste, Christoph Läsche, Cilli Sobiech, Eckard Böde, Axel Hahn

    Pages 146-161

12. Modular Automated Verification of Flexible Manufacturing Systems with Metric Temporal Logic and Non-Standard Analysis

    • Luca Ferrucci, Dino Mandrioli, Angelo Morzenti, Matteo Rossi

    Pages 162-176

13. Optimizing the Robustness of Software against Communication Latencies in Distributed Reactive Embedded Systems

    • Vlad Popa, Wolfgang Schwitzer

    Pages 177-191

14. A Formal Design of a Tool for Static Analysis of Upper Bounds on Object Calls in Java

    • Konrad Siek, Paweł T. Wojciechowski

    Pages 192-206

15. Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution

    • Jiří Slabý, Jan Strejček, Marek Trtík

    Pages 207-221

16. Back Matter

    PDF

This book constitutes the proceedings of the 17th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2012, held in Paris, France, in August 2012.
The 14 papers presented were carefully reviewed and selected from 37 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.

• Java
• embedded systems
• formal design
• program verification
• software engineering

• Department of Computer Science, Formal Methods and Tools, University of Twente, Enschede, The Netherlands

  Mariëlle Stoelinga

• Infrastructure and Cities Sector, Mobility and Logistics Division, Rail Automation, Siemens AG, Braunschweig, Germany

  Ralf Pinger

Policies and ethics