FTSCS 2014
Third International Workshop on Formal Techniques for Safety-Critical Systems

(An ICFEM 2014 Satellite Event)

Luxembourg, November 6 and 7, 2014

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

12:50 - 12:55 Closing

12:55 Lunch break