FTSCS 2013
Second International Workshop on Formal Techniques for Safety-Critical Systems

(An ICFEM 2013 Satellite Event)

Queenstown, New Zealand, October 29-30, 2013

Workshop Program for October 29 and October 30

Due to a large number of submissions, the program has been extended to two days (Oct. 29 - 30). The second day will run in parallel with ICFEM. The program for both days will run from 9:00 until 17:00, with the invited talk of ICFEM taking precedence on Oct. 30.

Day 1 (Tuesday October 29)

9:00 - 9:05 Welcome, opening

9:05 - 10:00 Invited talk: Ian Hayes (Chair: Cyrille Artho)

School of ITEE, The University of Queensland, Brisbane, Australia
Towards structuring system specifications with time bands using layers of rely-guarantee conditions

10:00 - 10:30 Coffee break

10:30 - 12:00 Model checking, model contracts (Chair: Toshiaki Aoki)

  • S. Ware, R. Malik, S. Mohajerani and M. Fabian
    Certainly Unsupervisable States
  • J. Suryadevara, G. Sapienza, C. Seceleanu, T. Seceleanu, S. Ellevseth and P. Pettersson
    Wind Turbine System: An Industrial Case Study in Formal Modeling and Verification
  • C. Wang, J. Ostroff and S. Hudon
    Precise Documentation and Validation of Requirements

12:00 - 13:30 Lunch break

13:30 - 15:00 Software, Industrial systems (Chair: Ian Hayes)

  • D. Pearce and L. Groves
    Reflections on Verifying Software with Whiley
  • X. Guo, H. Lin, K. Yatake and T. Aoki
    An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol
  • K. Hoque, O. Mohamed and Y. Savaria
    Early Analysis of Soft Error Effects for Aerospace Applications using Probabilistic Model Checking

15:00 - 15:30 Coffee break

15:30 - 17:00 Model checking (Chair: Cyrille Artho)

  • J. Ostroff, C. Wang, Y. Liu, J. Sun and S. Hudon
    TTM/PAT: Specifying and Verifying Timed Transition Models
  • A. Simpson and J. Jacobs
    On the cloud-enabled refinement checking of railway signalling interlockings
  • J. Nellen, E. Abraham, X. Chen and P. Collins
    Counterexample generation for hybrid automata

Day 2 (Wednesday October 30)

9:00 - 10:00 ICFEM Invited talk

10:00 - 10:30 Coffee break

10:30 - 12:00 Compositional verification, distributed systems (Chair: Robi Malik)

  • C. Pilbrow and R. Malik
    Compositional Nonblocking Verification with Always Enabled Events and Selfloop-only Events
  • L. Pang, C. Wang, M. Lawford and A. Wassyng
    Formalizing and Verifying Function Blocks using Tabular Expressions and PVS
  • Y. Sun, R. Soulat, G. Lipari, E. Andre and L. Fribourg
    Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems
  • 12:00 - 13:30 Lunch break

13:30 - 15:00 Modeling I (Chair: Jackie Wang)

  • G. Carvalho, F. Barros, F. Lapschies, U. Schulze and J. Peleska
    Model Based Testing from Controlled Natural Language Requirements
  • K. Traichaiyaporn and T. Aoki
    Refinement Tree and Its Patterns: a Graphical Approach for Event-B Modeling
  • Z. Kaviani, R. Khosravi, M. Sirjani, P. Olveczky and E. Khamespanah
    Formal Semantics and Analysis of Timed Rebeca in Real-Time Maude

15:00 - 15:30 Coffee break

15:30 - 17:00 Modeling II (Chair: Peter Ölveczky)

  • Y. Li and J. Pang
    A Strand Space Approach to Provable Anonymity
  • J. Bowen, S. Reeves and S. Jones
    Creating Visualisations of Formal Models of Interactive Medical Devices
  • C. Artho, K. Hayamizu, R. Ramler and Y. Yamagata
    With an Open Mind: How to Write Good Models