| Day 1 — Saturday, September 22nd | |
|---|---|
| 9:00 | Welcome |
| 9:15 | Keynote: Ernst-Rüdiger Olderog, Univ. of Oldenburg Automatic Verification of Combined Specifications (slides) |
| 10:15 | Coffee Break |
| Session: Software Models I (Zhiming Liu) | |
| 10:45 | Prototyping System Requirements Model (Xiaoshan Li) |
| 11:20 | A Rigorous Model of Service Component Architecture (Zuohua Ding, Jing Liu) |
| 11:55 | The Verification of rCOS Using SPIN (Xiao Yu, Zheng Wang) |
| 12:30 | Lunch (provided at UNU-IIST) |
| Session: (Anders P. Ravn) | |
| 14:30 | Integrating refinement into software development tools (Lu Yang) |
| 15:05 | An exercise on transition systems (Paula R. Ribeiro, Luis Barbosa, Shuling Wang) |
| 15:40 | Coffee Break |
| Session: Verification I (Naijun Zhan) | |
| 16:00 | On Verification of Linear Occurrence Properties of Real-Time Systems (Chang Il Choe, Van Hung Dang) |
| 16:35 | Parametric Analysis of an Improved Fault Tolerant System (Miaomiao Zhang) |
| Day 2 — Sunday, September 23rd | |
| Session: Verification II (Volker Stolz) | |
| 9:00 | Shape Analysis by Refining on Abstract Evaluation Path (Xiaodong Ma, Ji Wang, Wei Dong) |
| 9:35 | Engineering of An Assertion-based PSL-Verilog Dynamic Verifier by Alternating Automata (Naiyong Jin, Chengjie Shen, Jun Chen) |
| 10:10 | Coffee Break |
| Session: Software Models II (Geguang Pu) | |
| 10:30 | Barbed Model-Driven Software Development: A case study (Carlo Montangero, Laura Semini) |
| 11:05 | Generic tools via general refinement (Steve Reeves, David Streader) |
| 11:40 | Guest talk: Hybrid Systems (John Koo) |
| 12:30 | Lunch (provided at UNU-IIST) |
| 14:30 | Discussion I: Hybrid systems |
| 16:00 | Coffee Break |
| 16:30 | Discussion II: TTSS perspectives |
| 19:30 | Workshop Banquet (incl. in Registration) Restaurante Litoral, Rua do Almirante Sérgio, 261-A |