Formal Methods for Industrial Critical Systems

Invited Presentations.- Verification of Embedded Software: From Mars to Actions.- Synchronous Design and Verification of Critical Embedded Systems Using SCADE and Esterel.- Research Papers.- Static Analysis of the Accuracy in Control Systems: Principles and Experiments.- Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code.- Checking the TWIN Elevator System by Translating Object-Z to SMV.- Introducing Time in an Industrial Application of Model-Checking.- Integration of Formal Analysis into a Model-Based Software Development Process.- Formal Verification with Isabelle/HOL in Practice: Finding a Bug in the GCC Scheduler.- Computing Worst-Case Response Times in Real-Time Avionics Applications.- Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization.- An Action/State-Based Model-Checking Approach for the Analysis of Communication Protocols for Service-Oriented Applications.- Model Classifications and Automated Verification.- An Approach to Formalization and Analysis of Message Passing Libraries.- Analysis of a Session-Layer Protocol in mCRL2.- Automatic Certification of Java Source Code in Rewriting Logic.- Reverse Engineered Formal Models for GUI Testing.- Automatic Interoperability Test Case Generation Based on Formal Definitions.