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.
Author(s): Charles Pecheur (auth.), Stefan Leue, Pedro Merino (eds.)
Series: Lecture Notes in Computer Science 4916 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2008
Language: English
Pages: 254
Tags: Software Engineering; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Special Purpose and Application-Based Systems
Front Matter....Pages -
Verification of Embedded Software: From Mars to Actions....Pages 1-1
Synchronous Design and Verification of Critical Embedded Systems Using SCADE and Esterel....Pages 2-2
Static Analysis of the Accuracy in Control Systems: Principles and Experiments....Pages 3-20
Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code....Pages 21-37
Checking the TWIN Elevator System by Translating Object-Z to SMV....Pages 38-55
Introducing Time in an Industrial Application of Model-Checking....Pages 56-67
Integration of Formal Analysis into a Model-Based Software Development Process....Pages 68-84
Formal Verification with Isabelle/HOL in Practice: Finding a Bug in the GCC Scheduler....Pages 85-100
Computing Worst-Case Response Times in Real-Time Avionics Applications....Pages 101-114
Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization....Pages 115-132
An Action/State-Based Model-Checking Approach for the Analysis of Communication Protocols for Service-Oriented Applications....Pages 133-148
Model Classifications and Automated Verification....Pages 149-163
An Approach to Formalization and Analysis of Message Passing Libraries....Pages 164-181
Analysis of a Session-Layer Protocol in mCRL2....Pages 182-199
Automatic Certification of Java Source Code in Rewriting Logic....Pages 200-217
Reverse Engineered Formal Models for GUI Testing....Pages 218-233
Automatic Interoperability Test Case Generation Based on Formal Definitions....Pages 234-250
Back Matter....Pages -
