FTSCS 2019
Seventh International Workshop on Formal Techniques for Safety-Critical Systems

(An ICFEM 2019 Satellite Event)

Shenzhen, China, November 9, 2019


9:00 - 9:15: Opening

9:15 - 10:30: Invited talk: Sofiene Tahar: Formal Verification of Cyber-Physical Systems (Chair: Frederic Mallet)

10:30 - 11:00: Break

11:00 - 12:30: Session 1: Avionics and Spacecraft (chair: Frederic Mallet)

ˇ Neeraj Singh, Yamine Ait Ameur, Dominique Mery, David Navarre, Philippe Palanque, and Marc Pantel: Formal Development of Multi-Purpose Interactive Application (MPIA) for ARINC 661

ˇ Rodrigo Saar de Moraes and Simin Nadjm-Tehrani: Verifying Resource Adequacy of Networked IMA Systems at Concept Level

ˇ Shenghao Yuan, Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali, Tiexin Wang, and Yong Zhou: Automated Ada Code Generation from Synchronous Dataflow Programs on Multicore: Approach and Industrial Study

12:30 - 14:00: Lunch

14:00 - 15:30: Session 2: Applications (chair: Sofiene Tahar)

ˇ Dorra Ben Khalifa, Matthieu Martel, and Assale Adje: POP: A Tuning Assistant for Mixed-Precision Floating-Point Computations

ˇ Filippos Pantekis, Phillip James, Liam O'Reilly, Daniel Archambault, and Faron Moller: Visualising Railway Safety Verification

ˇ Elisabetta De Maria, Thibaud L'Yvonnet, Sabine Moisan, and Jean-Paul Rigault: Probabilistic activity recognition for serious games with applications in medicine

15:30 - 16:00: break

16:00 - 16:30: Session 3: Tools and Work in Progress (chair: Frederic Mallet)

ˇ Emily Yu, Martina Seidl, and Armin Biere: A Framework for CTLK Model Checking with QBF (Tool Paper)

ˇ Quang Thinh Trac and Mizuhito Ogawa: Formal Semantics Extraction from MIPS Instruction Manual (work in progress paper)

Workshop Program, November 16

8:45 - 9:00: Opening (with AWASE workshop)

9:00 - 9:45: AWASE keynote (Jifeng He)

9:45 - 10:00: Break

10:00 - 10:50: Session 1: Timing analysis (chair: Cyrille Artho)

  • Qurat Ul Ain and Osman Hasan:
    Formal Timing Analysis of Digital Circuits
  • Étienne André:
    A benchmarks library for parametric timed model checking

10:50 - 11:05: Break

11:05 - 12:20: Session 2: Decision, planning, optimization (chair: Cesar Munoz)

  • Liana Mikaelyan, Sascha Müller, Andreas Gerndt and Thomas Noll:
    Synthesizing and Optimizing FDIR Recovery Strategies From Fault Trees
  • John Törnblom and Simin Nadjm-Tehrani:
    Formal Verification of Random Forests in Safety-Critical Applications
  • Maryam Kamali, Sven Linker and Michael Fisher:
    Modular Verification of Vehicle Platooning with Respect to Decisions, Space and Time

12:20 - 13:30: Lunch

13:30 - 14:30: Invited talk: Cesar Munoz (chair Peter Ölveczky)

14:30 - 14:45: Break

14:45 - 15:35: Session 3: Refinement (chair: Osman Hasan)

  • Nils Timm and Stefan Gruner:
    Abstraction Refinement with Path Constraints for Three-Valued Bounded Model Checking
  • Karla Morris, Colin Snook, Thai Son Hoang, Rob Armstrong and Michael Butler:
    Refinement of Statecharts with Run-to-Completion Semantics

15:35 - 15:50: Coffee break

15:50 - 17:05: Session 4: Transformation and Analysis (chair: Étienne André)

  • William Bombardelli Da Silva, Max Bureck, Ina Schieferdecker and Christian Hein:
    Model Transformation with Triple Graph Grammars and Non-terminal Symbols
  • Yuanrui Zhang, Hengyang Wu, Yxchen Chen and Frederic Mallet:
    Embedding CCSL into Dynamic Logic: A Logical Approach for the Verification of CCSL Specifications
  • Asad Ahmed, Osman Hasan and Falah Awwad:
    Formal Stability Analysis of Control Systems

17:05 - 17:15: Closing