FMICS Schedule
Monday 15 Sept.
9:00-10:00 - Invited Talk
Formal Methods for Critical Systems
Steve Miller - Rockwell Collins
10:00-11:00 Testing
LETO - A Lustre-Based Test Oracle for Airbus Critical Systems
Wiels, Virginie; Durrieu, Guy; Waeselynck, Helene
Extending Structural Test Coverage Criteria for Lustre Programs with Multi-clock
Operators
Papailiopoulou, Virginia; Parissis, Ioannis; Du Bousquet, Lydie; Madani,
Laya
11:00-11:30 Coffee
11:30-13:00 Model Checking
Fighting State Space Explosion: Review and Evaluation
Pelanek, Radek;
Local Quantitative LTL Model Checking
Brim, Lubos; Tumova, Jana; Ceska, Milan; Cerna, Ivana; Barnat, Jiri
Efficient Symbolic Model Checking for Process Algebras
Vander Meulen, José; Pecheur, Charles
13:00-14:30 Lunch
14:30-15:30 Invited Talk
Model-Based Verification of Automotive Control Software
Rance Cleaveland - Department of Computer Science and Fraunhofer USA Center
for Experimental Software Engineering University of Maryland (FME keynote speaker)
15:30-16:00 Coffee
16:00-17:00 Case Studies
Reentrant Readers-Writers -- a Case Study Combining Model Checking
with Theorem Proving
Eekelen, Marko; Smetsers, Sjaak; Lensink, Leonard; Gastel, Bernard van
Using CSP||B Components: Application to a Platoon of Vehicles
Lanoix, Arnaud; Souquičres, Jeanine; Kouchnarenko, Olga; Colin, Samuel
17:00-18:00 Real-time
Formal Verification of the Implementability of Timing Requirements
Lawford, Mark; Wassyng, Alan; Hu, Xiayong
Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties
Colombo, Christian; Pace, Gordon J.; Schneider, Gerardo
20.00 Social dinner
Tuesday 16 Sept.
9:00-10:00 Invited Talk
Contract-Based Analysis of automotive and avionics applications: the SPEEDS
Approach
Werner Damm - OFFIS
10:00-11:00 Model Checking
Can Flash Memory Help In Model Checking?
Simecek, Pavel; Barnat, Jiri; Brim, Lubos; Edelkamp, Stefan; Sulewski, Damian
From Informal Requirements to Property-Driven Formal Validation
Roveri, Marco; Susi, Angelo; Tonetta, Stefano; Cimatti, Alessandro
11:00-11:30 Coffee
11:30-13:00 Panel Discussion on “Formal Methods in Commercial Software
Design Tools”, introduced by short presentations:
Model-driven software development: needs and experiences in rail automation
Milius, Stefan; Steinke, Uwe
Simulink Design Verifier vs. SPIN - A Comparative Case Study
Leitner, Florian; Leue, Stefan
13:00-14:30 Lunch
14:30-16:00 Verification
Automated Certification of Non-Interference in Rewriting Logic
Alpuente, Maria; Alba, Mauricio ; Escobar, Santiago
Formal Verification of Safety Functions by Reinterpretation of Functional Block
based Specifications
Bartha, Tamás; Németh, Erzsébet
Using Datalog and Boolean Equation Systems for Program Analysis
Joubert, Christophe; Villanueva, Alicia; Feliu, Marco; Alpuente, Maria
16:00-16:30 Coffee
16:30-18:00 ERCIM FMICS Working Group Meeting
