Preface

Conference Chairs (PDF)

pp. viii

Program Committee (PDF)

pp. ix

Referees (PDF)

pp. x

Keynote Speaker 1

From Requirements to Design: Formalizing the Key Steps (Abstract)

R.G. Dromey, Griffith University

pp. 2

PDF

Session 1: Testing

Supporting the Software Testing Process through Specification Animation (Abstract)

Tim Miller, University of Queensland

Paul Strooper, University of Queensland

pp. 14

PDF

Architecting Specifications for Test Case Generation (Abstract)

Richard Sinnott, University of Glasgow

pp. 24

PDF

Session 2: Formal Models for Security

Weak Bisimulation for Probabilistic Timed Automata and Applications to Security (Abstract)

Ruggero Lanotte, Università di Pisa

Andrea Maggiolo-Schettini, Università di Pisa

Angelo Troina, Università di Pisa

pp. 34

PDF

Refinement Operators and Information Flow Security (Abstract)

Annalisa Bossi, Università Caé Foscari di Venezia

Riccardo Focardi, Università Caé Foscari di Venezia

Carla Piazza, Università Caé Foscari di Venezia

Sabina Rossi, Università Caé Foscari di Venezia

pp. 44

PDF

A Formal Model for Trust in Dynamic Networks (Abstract)

Marco Carbone, University of Aarhus

Mogens Nielsen, University of Aarhus

Vladimiro Sassone, University of Sussex

pp. 54

PDF

Keynote Speaker 2

Taming Mobile Processes Using Types (Abstract)

Davide Sangiorgi, University of Bologna

pp. 64

PDF

Session 3: Program Verification

Facilitating Program Verification with Dependent Types (Abstract)

Hongwei Xi, Boston University

pp. 72

PDF

A Partial-Correctness Semantics for Modelling Assembler Programs (Abstract)

Geoffrey Watson, University of Queensland

Colin Fidge, University of Queensland

pp. 82

PDF

Program Verification Using Change Information (Abstract)

Bernhard Beckert, Universität Karlsruhe

Peter H. Schmitt, Universität Karlsruhe

pp. 91

PDF

Keynote Speaker 3

Towards a Well-Founded UML-Based Development Method (Abstract)

Egidio Astesiano, Università di Genova

Gianna Reggio, Università di Genova

pp. 102

PDF

Session 4: Integration of Formal and Informal Methods I

Behavioral Consistency Validation of UML Diagrams (Abstract)

Boris Litvak, Tel-Aviv University and IBM Research Center, Haifa

Shmuel Tyszberowicz, Tel-Aviv University and the Academic College of Tel-Aviv Yaffo

Amiram Yehudai, Tel-Aviv University and the Academic College of Tel-Aviv Yaffo

pp. 118

PDF

Component-Based Design and Analysis: A Case Study (Abstract)

Yan Jin, University of Adelaide

Charles Lakos, University of Adelaide

Robert Esser, University of Adelaide

pp. 126

PDF

Session 5: Integration of Formal and Informal Methods II

Towards Formalizing UML State Diagrams in CSP (Abstract)

Muan Yong Ng, University of Southampton

Michael Butler, University of Southampton

pp. 138

PDF

Semantic Properties of μ-Charts (Abstract)

Doug Goldson, University of Queensland

Greg Reeve, University of Waikato

pp. 148

PDF

The Fallacy of Spec-Based Design (Abstract)

Rahul Bhatt, Intel Corporation

Dave LaFollette, Intel Corporation

Arjun Kapur, Intel Corporation

pp. 156

PDF

Session 6: Object-Oriented Modelling

Formalizing the Framework Design Language F-UML (Abstract)

Nadia Bouassida, Institut Sup?rieur d?Informatique et de Multim?dias de Sfax

Han?ne Ben-Abdallah, Gestion de Sfax

Fa?ez Gargouri, Gestion de Sfax

Abdemajid Ben Hamadou, Institut Sup?rieur d?Informatique et de Multim?dias de Sfax

pp. 164

PDF

Modelling Java Concurrency with Object-Z (Abstract)

Roger Duke, University of Queensland

Luke Wildman, University of Queensland

Brad Long, University of Queensland

pp. 173

PDF

Specification Matching of Object-Oriented Components (Abstract)

Frank Feiks, Technical University of Berlin

David Hemer, University of Queensland

pp. 182

PDF

Animation of Object-Z Specifications Using a Z Animator (Abstract)

Tim McComb, University of Queensland

Graeme Smith, University of Queensland

pp. 191

PDF

Session 7: Automated Verification

Model Checking Visual Specification of Requirements (Abstract)

Ulka Shrotri, Tata Consultancy Services

Purandar Bhaduri, Tata Consultancy Services

R. Venkatesh, Tata Consultancy Services

pp. 202

PDF

Formal Verification of ASM Designs Using the MDG Tool (Abstract)

Amjad Gawanmeh, Concordia University

Sofiène Tahar, Concordia University

Kirsten Winter, University of Queensland

pp. 210

PDF

Light-Weight Theorem Proving for Debugging and Verifying Units of Code (Abstract)

David Déharbe, LORIA & INRIA-Lorraine and DIMAp/UFRN

Silvio Ranise, LORIA & INRIA-Lorraine

pp. 220

PDF

Author Index

Author Index (PDF)

pp. 229