| |
Wednesday, 5 November 2003
|
| |
7:45 - 8:45 |
Registration |
| |
8:45 - 9:00 |
Opening Ceremony |
| |
9:00 - 10:00 |
Keynote 1 |
| |
|
"Programs as paths",
Prof. Ian Hayes, University of Queensland, Australia |
| |
10:00 - 10:30 |
Break |
| |
10:30 - 12:30 |
Session 1:
Testing and Validation |
| |
|
10:30-11:00
"Working on Scenarios for Reproducible Testing"
Jessica Chen, University of Windsor, Canada |
| |
|
11:00-11:30
"AMBA-ARM7 Formal Verification Platform"
Kong Susanto, Univ. of Glasgow, UK
Tom Melham, Oxford University, UK |
| |
|
11:30-12:00
"Formalization, Testing and Execution of a Use Case Diagram"
Wuwei Shen, Western Michigan University, USA
Shaoying Liu, Hosei
University, Japan |
| |
|
12:00-12:30
"Services-Based Systems Engineering: Consistent Combination of Services"
Bernhard Schätz, TU Mščnchen, Germany
Christian Salzmann, BMW Car-IT, Germany |
| |
12:30 -
14:00 |
Lunch |
| |
14:00 -
15:30 |
Session 2:
State Diagrams |
| |
|
14:00-14:30
"Using state diagrams to describe concurrent behaviour"
Jim Davies, Charles Crichton, University of Oxford, UK |
| |
|
14:30-15:00
"The equivalence of Statecharts"
Quan Long, Zongyan Qiu, Peking University, China
Shengchao Qin, Singapore-MIT Alliance, National University of Singapore,
Singapore
|
| |
|
15:00-15:30
"Generic Interacting State Machines and their instantiation with dynamic
features"
David von Oheimb, Volkmar Lotz, Siemens CT IC Sec, Germany |
| |
15:30
- 16:00 |
Break |
| |
16:00
- 17:30 |
Session
3: PVS/HOL |
| |
|
16:00-16:30
"Using PVS to prove Properties of Systems Modelled in a Synchronous Dataflow
Language"
Sanjai Rayadurgam, Anjali Joshi, Mats Heimdahl, University of
Minnesota, USA |
| |
|
16:30-17:00 "Formalising
an Integrated Language in PVS"
Gwen Salaščn, Christian AttiogbšŠ, IRIN, France |
| |
|
17:00-17:30
"Modeling SystemC Fixed-Point Arithmetic in HOL"
Behzad Akbarpour, Sofiene Tahar, Concordia University, CANADA |
| |
18:30 - ? |
Reception,
TBC |
| |
|
| |
Thursday, 6 November 2003
|
| |
9:00 - 10:00
|
keynote 2
|
| |
|
"Model Based Formal Code Verification"
Dr.
Colin O'Halloran, QinetiQ, UK |
| |
10:00 - 10:30
|
Break |
| |
10:30 -
12:30 |
Parallel
session 4A: Refinement |
| |
|
10:30-11:00
"Adding action refinement to stochastic true concurrency models"
Mila Majster-Cederbaum, Jinzhao Wu, Universitaet Mannheim, Germany |
| |
|
11:00-11:30
"Incremental derivation of abstraction relations for data refinement"
Neil Robinson, The University of Queensland, Australia |
| |
|
11:30-12:00
"Comparison of data and process refinement"
David Streader, Steve Reeves, University of Waikato, NZ |
| |
|
12:00-12:30
"Compilation by Refinement for a Practical Assembly Language"
Geoffrey Watson, The University of Queensland, Australia |
| |
10:30 -
12:30 |
Parallel
session 4B: Hybrid Systems |
| |
|
10:30-11:00
"Java Card Code Generation from B Specifications"
Bruno Tatibouet, Jean-Christophe Voisinet, Ahmed Hammad University of Franche-Comte,
France
Antoine Requet, Gemplus
Research Laboratory, France |
| |
|
11:00-11:30
"Efficient Path Finding with the Sweep-Line Method using External Storage"
Lars Kristensen, Thomas Mailund, University of Aarhus,Denmark |
| |
|
11:30-12:00 "Formal
development of a distributed logging mechanism supporting disconnected updates"
Yuechen QIAN, Philips Research Laboratories, Netherlands |
| |
|
12:00-12:30
"Formal proof of a polychronous protocol for loosely time-triggered
architectures"
Mickael Kerboeuf, NSA-Rennes, France
David Nowak, CNRS,ENS Cachan, France
Jean-Pierre Talpin, INRIA, France |
| |
12:30 -
14:00 |
Lunch |
| |
14:00 -
15:30 |
Parallel
session 5A: Z/Object-Z |
| |
|
14:00-14:30
"A Z Based Approach to Verifying Security Protocols"
Benjamin Long, Colin Fidge, Antonio Cerone, The University of Queensland,
Australia |
| |
|
14:30-15:00
"A Refinement Tool for Z"
Angela Freitas, Carla Nascimento, Centro de Informatica - Universidade Federal
de Pernambuco, Brazil
Ana Cavalcanti, University of Kent, UK |
| |
|
15:00-15:30
"The Common Semantic Constructs of XML Family"
Yang Hong Li, Hao Ke Gang, Northwest University, China
Han Jun Gang, University of Xi'an Post & Telecomm, China |
| |
14:00 -
15:30 |
Parallel
session 5B: Petri Nets |
| |
|
14:00-14:30
"Controller Synthesis for Object Petri Nets"
Berndt Farwer, Universitat Hamburg, UK
Saraswati Kalvala, Kundan Misra, University of Warwick, UK |
| |
|
14:30-15:00 "Towards
a Workflow Model of Real-Time Cooperative Systems"
Yuyue Du, Changjun Jiang, Tongji University, China |
| |
|
15:00-15:30 "New
Developments in Closed-Form Computation for GSPN Aggregation"
Jonathan Billington,University of South Australia, Australia |
| |
15:30 -
16:00 |
Break |
| |
16:00 -
17:30 |
Session 6:
Timed Automata |
| |
|
16:00-16:30
"On Clock Difference Constraints and Termination in Reachability Analysis of
Timed Automata"
Johan Bengtsson, Wang Yi, Uppsala University, Sweden |
| |
|
16:30-17:00
"Analyzing the Redesign of a Distributed Lift System in UPPAAL"
Jun Pang, Bart Karstens, CWI
Wan Fokkink, CWI and Vrije Universiteit
Amsterdam, The Netherlands |
| |
|
17:00-17:30
"Verification of Timeliness QoS Properties in Multimedia Systems"
Behzad Bordbar,University of Birmingham, UK
Kozo Okano, Osaka University, Japan |
| |
18:30 - ? |
Dinner
at Singapore Zoological Garden and Night Safari tour, TBC |
| |
|
|
| |
Friday, 7 November 2003
|
| |
9:00 - 10:00
|
Keynote 3
|
| |
|
"TBA"
Dr. Mathai Joseph, Tata Research
Development & Design Centre, India |
| |
10:00 -
10:30 |
Break |
| |
10:30 -
12:30 |
Session 7:
System Modeling and Checking |
| |
|
10:30-11:00
"A Calculus for Set-Based Program Development"
Georg Struth,Universität Augsburg, Germany |
| |
|
11:00-11:30
"Compositional Verification of a Switch Fabric from Nortel Networks"
Hong Peng, Sofiene Tahar, Yassine Mokhtari, Concordia University, Montreal,
Canada |
| |
|
11:30-12:00
"Constraint-Based Model Checking of Data-Independent Systems"
Beata Sarna-Starosta, C.R. Ramakrishnan, SUNY Stony Brook, USA |
| |
|
12:00-12:30
"A Formal Model for the Block Subsystems of the Linux Kernel"
Peter Breuer, Universidad Carlos III de Madrid, Spain |
| |
12:30 -
14:00 |
Lunch
|
| |
14:00 -
15:30 |
Session 8:
Semantics and Synthesis |
| |
|
14:00-14:30
"A Mathematical Framework for Safecharts"
Hamdan Dammag, Nimal Nissanke, South Bank University, UK |
| |
|
14:30-15:00
"A Relational Model for Formal Object-Oriented Requirement Analysis in UML"
Zhiming Liu, Jifeng He, UNU/IIST, Macau
Xiaoshan Li, University of Macau, Macau
Yifeng Chen, University of Leicester, |
| |
|
15:00-15:30
"FROM SPECIFICATION TO HARDWARE DEVICE: A SYNTHESIS ALGORITHM"
VINCENZA CARCHIOLO, MICHELE MALGERI, GIUSEPPE MANGIONI, DIPARTIMENTO DI INGEGNERIA INFORMATICA E DELLE TELECOMUNICAZIONI,
ITALY |
| |
15:30 -
16:00 |
Break |
| |
16:00 -
17:30 |
Session 9:
Panel and Closing |
| |
18:30 - ?
|
Santosa
Event, Musical Fountain Show, TBC
(optional) |
| |
|
|
 |
Site last
revised on Saturday, 19 July 2003. |
|
| |
