FMICS 2009 - PRELIMINARY PROGRAM Please visit: http://users.dsic.upv.es/workshops/fmics2009 ************************************************************ * 14th International Workshop on * * Formal Methods for Industrial Critical Systems * * FMICS 2009 * * * * November 2-3, 2009 * * Eindhoven, The Netherlands * ************************************************************ Monday 2 November ***************** 9h-10h Invited Talk (Chair: XXX) Ken McMillan Cadence, USA What's in Common Between Test, Model Checking, and Decision Procedures? ********************** 10h-10h30 Coffee Break ********************** 10h30-11h30 Session 1 (Chair: XXX) David Delmas, Eric Goubault, Sylvie Putot, Jean Souyris, Karim Tekkal and Franck Vedrine. Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software Alwyn Goodloe and Cesar Munoz. Compositional Verification of a Communication Protocol for a Remotely Operated Vehicle 11h30-12h Poster Session 1 (Chair: XXX) Alessio Ferrari, Alessandro Fantechi, Stefano Bacherini and Niccolo Zingoni. Formal Development for Railway Signaling Using Commercial Tools Nassima Izerrouken, Marc Pantel, Xavier Thirioux and Olivier Ssi Yan Kai. Integrated Formal Approach for Qualified Critical Embedded Code Generator Laura Panizo, Maria del Mar Gallardo, Pedro Merino and Antonio Linares. Developing a Decision Support Tool for Dam Management with SPIN ***************** 12h30-14h30 Lunch ***************** 14h30-15h30 Invited Talk (Chair: XXX) Dino Distefano Queen Mary, University of London, UK Attacking Large Industrial Code with Bi-Abductive Inference ********************** 15h30-16h Coffee Break ********************** 16h-17h30 Session 2 (Chair: XXX) Jose Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto and Bárbara Vieira. Correctness with Respect to Reference Implementations Erik Schierboom, Alejandro Tamalet, Hendrik Tews, Marko van Eekelen and Sjaak Smetsers. Preemption Abstraction: a Lightweight Approach to Modelling Concurrency. Javier de Dios and Ricardo Pena. A Certified Implementation on top of the Java Virtual Machine *********************************** 19h Workshop Dinner and EASST award *********************************** Tuesday 3 November ****************** 9h-10h Invited Talk (Chair: XXX) Diego Latella ISTI/CNR, Italy On a Uniform Framework for the Definition of Stochastic Process Languages ********************** 10h-10h30 Coffee Break ********************** 10h30-12h Session 3 (Chair: XXX) Matthias Raffelsieper, MohammadReza Mousavi, Jan-Willem Roorda, Chris Strolenberg and Hans Zantema. Formal Analysis of Non-Determinism in Verilog Cell Library Simulation Models Julio Marino, Angel Herranz, Manuel Carro and Juan Jose Moreno-Navarro. Formal Modeling of Concurrent Systems with Shared Resource Kenneth J. Turner and Koon Leai Larry Tan. A Rigorous Methodology for Composing Services ***************** 12h30-14h30 Lunch ***************** 14h30-15h30 Invited Talk (Chair: XXX) Thierry Lecomte ClearSy, France Applying a Formal Method in Industry: a 15-year trajectory 15h30-16h Poster Session 2 (Chair: XXX) Lukas Ladenberger, Jens Bendisposto and Michael Leuschel. Visualizing Event-B models with BMotionStudio Wojciech Mostowski, Erik Poll, Julien Schmaltz, Jan Tretmans and Ronny Wichers Schreur. Model-Based Testing of Electronic Passports Aad Mathijssen, Yaroslav S. Usenko and Dragan Bosnacki. Behavioural Analysis of an I2C Linux Driver ********************** 16h-16h30 Coffee Break ********************** 16h30-17h30 Session 4 (Chair: XXX) Pavel Parizek and Tomas Kalibera. Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs Sami Evangelista and Lars Michael Kristensen. Dynamic State Space Partitioning for External Memory Model Checking 17h30-18h30 FMICS Working Group meeting and closure