FTSCS 2012
First International Workshop on Formal Techniques for Safety-Critical Systems

(An ICFEM 2012 Satellite Event)

Kyoto, Japan, November 12, 2012


  • 09:00 to 09:05 - Welcome/opening
  • 09:05 to 10:00 - Invited talk (Chair: Cyrille Artho)
  • 10:00 to 10:30 - Ad hoc networks (Chair: Cyrille Artho)
    • Mengying Wang and Yang Lu
      A Timed Calculus for Mobile Ad Hoc Networks
  • 10:30 to 11:00 - Coffee break
  • 11:00 to 12:00 - Real-time systems (Chair: Sofiène Tahar)
    • Kyungmin Bae, Joshua Krisiloff, José Meseguer and Peter Ölveczky
      PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude
    • Peter Hui and Satish Chikkagoudar
      Formal Verification of Temporal Properties In Real-Time Parallel Computation
  • 12:00 to 13:20 - Lunch break
  • 13:20 to 14:20 - Software/systems analysis I (Chair: Ralf Huuck)
    • Adrien Champion, Rémi Delmas and Michael Dierkes
      Generating Property Directed Potential Invariants By Backward Analysis
    • Mingyu Park, Taejoon Byun and Yunja Choi
      Property-based Code Slicing for Efficient Verification of OSEK/VDX Operating Systems
  • 14:20 to 14:30 - Short break
  • 14:30 to 15:30 - Software/systems analysis II (Chair: Takashi Kitamura)
    • Masahiro Matsubara, Kohei Sakurai, Fumio Narisawa, Masushi Enshoiwa, Yoshio Yamane and Hisamitsu Yamanaka
      Model Checking with Program Slicing Based on Variable Dependence Graph
    • Siraj A. Shaikh and Paddy Krishnan
      A Framework for Analysing Driver Interactions with Semi-Autonomous Vehicles
  • 15:30 to 16:00 - Coffee break
  • 16:00 to 17:00 - Modeling, Model-driven Engineering (Chair: Tatsuhiro Tsuchiya)
    • Chen-Wei Wang and Jim Davies
      Formal Model-Driven Engineering: Generating Data and Behavioural Components
    • Zheng Wang, Geguang Pu, Shengchao Qin, Jianwen Li, Kim Guldstrand Larsen, Jan Madsen, Bin Gu and Jifeng He
      MDM: A Mode Diagram Modeling Framework for Periodic Control Systems
  • 17:00 to 17:05 - Short break
  • 17:05 to 18:05 - Short presentations (Chair: Peter Ölveczky)
    • Mohamed Yousri Mahmoud, Vincent Aravantinos and Sofiène Tahar
      Towards the Formal Verification of Quantum Optical Systems
    • Jagadish Suryadevara and Ling Yin
      Timed Automata Modeling of CCSL Constraints
    • Maria Spichkova and Alarico Campetelli
      Towards system development methodologies: From software to cyber-physical domain
  • 18:05 to 18:10 - Closing