| |
|
Conference Theme |
| |
Formal methods for developing computing systems have been extensively researched
and their use in industry is increasing. Recent applications to the development
of mission-critical, safety-critical and security-critical systems have
significantly increased trustworthiness, without increasing overall development
costs.
The challenge now is to achieve general
acceptance of formal methods as a part of industrial development of high quality
systems, particularly trusted systems. More needs to be known about merging
formal methods into industrial engineering practice, including new and emerging
practice. This includes increasing productivity of formal engineering methods,
for example through improved tool support.
ICFEM 2003 aims to bring together researchers and practitioners from industry,
academia, and government to advance the state of the art in formal engineering
methods and to encourage wider uptake of formal methods in industry.
The conference will benefit from the contributions of three distinguished
invited speakers. 34 high quality papers (selected from 91 submissions) will
also be presented, drawn from a wide range of subjects including modeling,
refinement, testing and verification. |
| |
Conference Preliminary Program |
| |
Wednesday, 5 November 2003
|
| |
7:45 - 8:45 |
Registration |
| |
8:45 - 9:00 |
Opening Ceremony
(chair: P.S. Thiagarajan) |
| |
9:00 - 10:00 |
Keynote 1
(details)
(chair: Jin Song Dong) |
| |
|
"Programs as paths",
Prof. Ian Hayes, University of Queensland, Australia |
| |
10:00 - 10:30 |
Break |
| |
10:30 - 12:30 |
Session 1:
Testing and Validation (chair: Wang Yi) |
| |
|
10:30-11:00
"Using Formal Methods to Serialize
Synchronization Events"
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 Schatz, TU Munchen, Germany
Christian Salzmann, BMW Car-IT, Germany |
| |
12:30 -
14:00 |
Lunch |
| |
14:00 -
15:30 |
Session 2:
State Diagrams (chair: Zhiming Liu) |
| |
|
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 (chair: Hugh Anderson) |
| |
|
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 Salaun, Christian Attiogbe, IRIN, France |
| |
|
17:00-17:30
"Modeling SystemC Fixed-Point Arithmetic in HOL"
Behzad Akbarpour, Sofiene Tahar, Concordia University, CANADA |
| |
18:30 - |
Welcome
dinner (Cafe des Artistes, The Oriental Hotel) |
| |
|
| |
Thursday, 6 November 2003
|
| |
9:00 - 10:00
|
Keynote 2
(details)
(chair: Jim Woodcock) |
| |
|
"Model Based Formal Code Verification"
Dr.
Colin O'Halloran, QinetiQ, UK |
| |
10:00 - 10:30
|
Break |
| |
10:30 -
12:30 |
Parallel
session 4A: Refinement (chair: Jim Davies) |
| |
|
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 (chair: Sofiene Tahar) |
| |
|
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/UML (chair: Shaoying Liu) |
| |
|
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, Universidade Federal
de Pernambuco, Brazil
Ana Cavalcanti, University of Kent, UK |
| |
|
15:00-15:30
"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, UK |
| |
14:00 -
15:30 |
Parallel
session 5B: Petri Nets and Timed Automata (chair: Abhik Roychoudhury) |
| |
|
14:00-14:30
"Verification of Timeliness QoS Properties in Multimedia Systems"
Behzad Bordbar,University of Birmingham, UK
Kozo Okano, Osaka University, Japan |
| |
|
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"
Jorn Freiheit, Jonathan Billington,University of South Australia, Australia |
| |
15:30 -
15:45 |
Break |
| |
15:45 -
17:15 |
Session 6:
Timed Automata (chair: Martin Henz) |
| |
|
15:45-16:15
"On Clock Difference Constraints and Termination in Reachability Analysis of
Timed Automata"
Johan Bengtsson, Wang Yi, Uppsala University, Sweden |
| |
|
16:15-16:45
"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:30 - |
Conference
dinner at Singapore
Zoological Garden and Night Safari tour |
| |
|
|
| |
Friday, 7 November 2003
|
| |
9:00 - 10:00
|
Keynote 3
(details)
(chair: P.S. Thiagarajan) |
| |
|
"Adding
Formalism to Methods or Where and When Will Industry Use Formal Reasoning?"
Dr. Mathai Joseph, Tata Research
Development & Design Centre, India |
| |
10:00 -
10:30 |
Break |
| |
10:30 -
12:30 |
Session 7:
System Modeling and Checking (chair: Ana Cavalcanti) |
| |
|
10:30-11:00
"A Calculus for Set-Based Program Development"
Georg Struth,Universitat Augsburg, Germany |
| |
|
11:00-11:30
"Compositional Verification of a Switch Fabric from Nortel Networks"
Hong Peng, Sofiene Tahar, Yassine Mokhtari, Concordia University,
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:00 |
Session 8:
Semantics and Synthesis (chair: Shengchao Qin) |
| |
|
14:00-14:30
"A Mathematical Framework for Safecharts"
Hamdan Dammag, Nimal Nissanke, South Bank University, UK |
| |
|
14:30-15:00
"From Specification to Hardware Device: A Synthesis Algorithms"
Vincenza Carchiolo, Michele Malgeri, Giuseppe Mangioni, Dipartimento Di
Ingegneria
Informatica E Delle Telecomunicazioni, Italy |
| |
15:00-15:30 |
Closing session (Jim Woodcock and Jim
Davies) |
| |
16:00 - |
Sentosa
Island
Event, TBC
(optional) |
| |
|
|
| |
Dinner Information |
| |
|
Welcome Dinner:
Cafe des Artistes, The Oriental Hotel,
5 Raffles Avenue, Marina Square
(neighbour hotel to the conference site, walking distance) |
Conference Dinner:
at Singapore Zoological Garden and Night Safari tour
Bus will leave from the conference hotel at 17:30 and come back to
conference hotel and NUS visitor lodge at 22:30 |
|
 |
Site last
revised on Saturday, 19 July 2003. |
|
| |
