Workshop Program for November 6 and 7
Day 1 (Friday November 6, Room 21.2.23)
09:00 - 09:05 Welcome/opening
09:05 - 10:00 Invited talk: José Meseguer (Chair: Peter Ölveczky)
University of Illinois
Towards Extensible Symbolic Formal Methods
10:00 - 10:30 Coffee break
10:30 - 12:00 Clocks, real time, Plasma Lab (Chair: Sofiène Tahar)
- Min Zhang and Frederic Mallet.
An Executable Semantics of Clock Constraint Specification Language and its Applications - Étienne André.
What's decidable about parametric timed automata? (SURVEY) - Jalil Boudjadar, Juergen Dingel, Boris Madzar and Jin Hyun Kim.
Compositional Predictability Analysis of Mixed Critical Real Time Systems - Louis-Marie Traonouez and Axel Legay.
Statistical Model Checking of Simulink Models with Plasma Lab
12:05 - 13:30 Lunch
13:30 - 15:00 Theory, methodology (Chair: Toshiaki Aoki)
- Klaus Becker and Sebastian Voss.
A Formal Model and Analysis of Feature Degradation in Fault-Tolerant Systems - Hsin-Hung Lin, Yoichi Omori, Shigeru Kusakabe and Keijiro Araki.
Towards Verifying VDM using SPIN - Jackson R. Mayo, Robert C. Armstrong and Geoffrey C. Hulette.
Leveraging Abstraction to Establish Out-of-Nominal Safety Properties - Mattias Ulbrich, Schreiter Luzie, Sarah Grebing, Jörg Raczkowsky, Heinz Wörn and Bernhard Beckert.
A Concept for Multi-Phase Incremental Formal Verification in Robotic Guided Surgery
15:05 - 15:30 Coffee break
15:30 - 16:40 Automotive, avionics (Chair: Frédéric Mallet)
- Toshiaki Aoki, Kriangkrai Traichaiyaporn, Yuki Chiba, Masahiro Matsubara, Masataka Nishi and Fumio Narisawa.
Modeling Safety Requirements of ISO26262 using Goal Trees and Patterns - Majdi Ghadhab, Matthias Kuntz, Dmitrii Kuvaiskii and Christof Fetzer.
A Controller Safety Concept based on Software-Implemented Fault Tolerance for Fail-Operational Automotive Applications - Toby Wilkinson, Michael Butler, Martin Paxton and Xanthippe Waldron.
A Formal Approach to Multi-UAV Route Validation
Day 2 (Saturday November 7, Room 17.2.15)
9:30 - 10:45 Railway systems (Chair: Étienne André)
- Phillip James, Andrew Lawrence, Markus Roggenbach and Monika Seisenberger.
Towards safety analysis of ERTMS/ETCS Level 2 in Real-Time Maude - Stefan Gruner, Abby Kumar and Tom Maibaum.
Towards a Body of Knowledge in Formal Methods for the Railway Domain: Identification of Settled Knowledge - Roberto Nardone, Ugo Gentile, Massimo Benerecetti, Adriano Peron, Valeria Vittorini, Stefano Marrone and Nicola Mazzocca.
Modeling Railway Control Systems in Promela
10:45 - 11:15 Coffee break
11:15 - 12:25 Software, wireless networks, g-HOL (Chair: Cyrille Artho)
- Pablo Gonzalez De Aledo and Ralf Huuck.
An Approach to Static-Dynamic Software Analysis - Xi Wu and Huibiao Zhu.
Probabilistic Analysis of a Calculus for Wireless Sensor Networks - Fahd Arshad, Hassan Mehmood, Osman Hasan and Fauzan Raza.
g-HOL - A Graphical User Interface for the HOL Proof Assistant