Workshop on Formal Methods in Aerospace

08:30 [Coffee available]

09:05 Plenary lecture: Klaus Havelund (Jet Propulsion Laboratory, USA) and Howard Barringer (Manchester, UK) - Runtime Verification of Log Files - a Trojan horse for Formal Methods

09:55 Contributed paper: Gopinadh Sirigineedi, Antonios Tsourdos, Rafal Zbikowski and Brian A. White (Cranfield, UK) - Modelling and Verification of Multiple UAV Mission Using SMV

10:20 BREAK

10:40 Plenary lecture: Henk Blom (National Aerospace Laboratory, NL) - Probabilistic Safety Verification of Future Air Traffic Management

11:30 Contributed paper: Julien Forget, Frederic Boniol, David Lesens and Claire Pagetti (ONERA, France). - Implementing Multi-Periodic Critical Systems: from Design to Code Generation

11:55 Contributed paper: Piotr Kordy, Rom Langerak and Jan Willem Polderman (Twente, NL) - Re-verification of a Lip Synchronization Protocol using Robust Reachability

12:20 LUNCH

13:30 Special Track on ongoing projects and new research trends (I)

• 13:30 Nick Lincoln and Sandor Veres (Southampton, UK) - Agent Reasoning Beyond Logic - Abstractions of a 6DOF spacecraft

• 13.55 Marika Di Benedetto, S. Di Gennaro, and Alessandro D'Innocenzo (L'Aquila, IT) - Observability and diagnosability of hybrid systems with application in Air Traffic Management

• 14:20 Alessandro Cimatti, Marco Roveri, Angelo Susi and Stefano Tonetta (FBK Trento, IT) - Formalization and validation of safety-critical requirements

• 14:45 Mircea Lazar (Eindhoven, NL) - Flexible Lyapunov Functions and Applications to Fast Mechatronic Systems

15:10 BREAK

15:30 Special Track on ongoing projects and new research trends (II)

• 15.30 Louise Dennis (Liverpool, UK) - Agent Based Approaches to Engineering Autonomous Space Software

• 15:55 Thierry Gautier and Jean-Pierre Talpin (INRIA Rennes, FR) - Synoptic: a domain-specific modeling language for space on-board application software

• 16:20 Emil Vassev and Mike Hinchey (UCD & Lero, IE) - Developing Experimental Models for NASA Missions with ASSL

• 16:45 Pieter Collins, Jan H. van Schuppen, Bert van Beek, Davide Bresolin, Ivan Zapreev, and Sanja Zivanovic (CWI, NL) - Model Checking Nonlinear Hybrid Systems

• 17:05 Alessandro Abate (Delft, NL) - Abstractions for stochastic hybrid systems

17:30 Closing