Workshop Program for November 6 and 7
Day 1 (Thursday November 6)
9:10 - 9:15 Welcome, opening
9:15 - 10:15 Invited talk: Klaus Havelund (Chair: Cyrille Artho)
NASA Jet Propulsion Laboratory (JPL)
Experience with Rule-Based Analysis of Spacecraft Logs
10:15 - 10:40 Coffee break
10:40 - 12:20 Concurrency in hardware and systems (Chair: Klaus Havelund)
- Timon Kelter and Peter Marwedel
Parallelism Analysis: Precise WCET Values for Complex Multi-Core Systems - Syed Ali Asadullah Bukhari, Faiq Khalid Lodhi, Osman Hasan, Muhammad Shafique, and Joerg Henkel
Formal Verification of Distributed Task Migration for Thermal Management in On-chip Multi-core Systems using nuXmv - Frederic Mallet and Grygoriy Zholtkevych
Coalgebraic Semantic Model for the Clock Constraint Specification Language - Damian Adalid, Maria del Mar Gallardo and Laura Titolo
Modelling Hybrid Systems in Hy-tccp
12:20 - 14:00 Lunch break
14:00 - 15:15 Railway systems (Chair: Peter Ölveczky)
- Linh H. Vu, Anne E. Haxthausen, and Jan Peleska
Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release - Ugo Gentile, Roberto Nardone, Adriano Peron, Valeria Vittorini, Stefano Marrone, Renato De Guglielmo, Nicola Mazzocca, and Luigi Velardi
Dynamic State Machines for Formalizing Railway Control System Specifications - Andrew Lawrence, Ulrich Berger, Phillip James, Markus Roggenbach, and Monika Seisenberger
Modelling and Analysing the European Rail Traffic Management System in Real-Time Maude
15:15 - 15:45 Coffee break
15:45 - 17:00 Program analysis (Chair: Thomas Noll)
- Georgiana Caltais
Expression-based aliasing for OO-languages - Amira Methni, Matthieu Lemerre, Belgacem Ben Hedia, Serge Haddad, and Kamel Barkaoui
Specifying and Verifying Concurrent C Programs with TLA+ - Raluca Marinescu, Cristina Seceleanu, Henrik Lonn, Henrik Kaijser, Marius Mikucionis, and Alexandre David
Analyzing Industrial Architectural Models by Simulation and Model-Checking
18:00 - 21:00 Workshop dinner (optional)
Day 2 (Friday November 7)
9:15 - 10:15 Invited talk: Thomas Noll (Chair: Peter Ölveczky)
RWTH Aachen University
Safety, Dependability and Performance Analysis of Aerospace Systems
10:15 - 10:40 Coffee break
10:40 - 11:55 Protocol analysis; refinement checking, automata (Chair: Frederic Mallet)
- Dominik Klein
Key-Secrecy of PACE with OTS/CafeOBJ - Mamoun Filali-Amine, Meriem Ouederni, and Jean-Baptiste Raclet
A Normalized Form for FIFO Protocols Traces, Application to the Replay of Mode-based Protocols - Jaco Jacobs and Andrew Simpson
A Formal Model of SysML Blocks using CSP for Assured Systems Engineering
12:00 - 12:50 Automotive systems (Chair: Cyrille Artho)
- Haitao Zhang, Toshiaki Aoki, and Yuki Chiba
A Spin-based Approach for Checking OSEK/VDX Applications - Vu Huong, Yuki Chiba, Kenro Yatake, and Toshiaki Aoki
Checking the Conformance of a Promela Design to Its Formal Specification in Event-B