Formal Methods for Industrial Critical Systems

1. Front Matter

   PDF

2. Invited Presentations

   1. Verification of Embedded Software: From Mars to Actions

      • Charles Pecheur

      Pages 1-1

   2. Synchronous Design and Verification of Critical Embedded Systems Using SCADE and Esterel

      • Gérard Berry

      Pages 2-2

3. Research Papers

   1. Static Analysis of the Accuracy in Control Systems: Principles and Experiments

      • Eric Goubault, Sylvie Putot, Philippe Baufreton, Jean Gassino

      Pages 3-20

   2. Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code

      • Bastian Schlich, Jann Löll, Stefan Kowalewski

      Pages 21-37

   3. Checking the TWIN Elevator System by Translating Object-Z to SMV

      • Sören Preibusch, Florian Kammüller

      Pages 38-55

   4. Introducing Time in an Industrial Application of Model-Checking

      • Lionel van den Berg, Paul Strooper, Kirsten Winter

      Pages 56-67

   5. Integration of Formal Analysis into a Model-Based Software Development Process

      • Michael Whalen, Darren Cofer, Steven Miller, Bruce H. Krogh, Walter Storm

      Pages 68-84

   6. Formal Verification with Isabelle/HOL in Practice: Finding a Bug in the GCC Scheduler

      • Lars Gesellensetter, Sabine Glesner, Elke Salecker

      Pages 85-100

   7. Computing Worst-Case Response Times in Real-Time Avionics Applications

      • Murali Rangarajan, Darren Cofer

      Pages 101-114

   8. Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization

      • Leonard Lensink, Sjaak Smetsers, Marko van Eekelen

      Pages 115-132

   9. An Action/State-Based Model-Checking Approach for the Analysis of Communication Protocols for Service-Oriented Applications

      • Maurice H. ter Beek, A. Fantechi, S. Gnesi, F. Mazzanti

      Pages 133-148

   10. Model Classifications and Automated Verification

       • Radek Pelánek

       Pages 149-163

   11. An Approach to Formalization and Analysis of Message Passing Libraries

       • Robert Palmer, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby

       Pages 164-181

   12. Analysis of a Session-Layer Protocol in mCRL2

       • Marko van Eekelen, Stefan ten Hoedt, René Schreurs, Yaroslav S. Usenko

       Pages 182-199

   13. Automatic Certification of Java Source Code in Rewriting Logic

       • Mauricio Alba-Castro, María Alpuente, Santiago Escobar

       Pages 200-217

   14. Reverse Engineered Formal Models for GUI Testing

       • Ana C. R. Paiva, João C. P. Faria, Pedro M. C. Mendes

       Pages 218-233

   15. Automatic Interoperability Test Case Generation Based on Formal Definitions

       • Alexandra Desmoulin, César Viho

       Pages 234-250

4. Back Matter

   PDF

This book constitutes the thoroughly refereed post-workshop proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2007, held in Berlin, Germany, in July 2007 - colocated with CAV 2007, the 19th International Conference on Computer Aided Verification. The 15 revised full papers presented together with the abstracts of 2 invited lectures were carefully selected during two rounds of reviewing and improvement from 31 initial submissions. The papers strive to promote research and development for the improvement of formal methods and tools for industrial applications and they are organized in topical sections on control systems, scheduling and time, verification, software, and testing.

• Computer
• Java
• calculus
• cyclic scheduling
• distributed verification
• embedded systems
• formal method
• formal specification
• formal verification
• microcontroller
• model-based development
• real-time
• real-time analysis
• software verifi
• verification

Policies and ethics