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