The Community for Technology Leaders
Engineering of Complex Computer Systems, IEEE International Conference on (2007)
Auckland, New Zealand
July 11, 2007 to July 14, 2007
ISBN: 0-7695-2895-3
TABLE OF CONTENTS
Introduction

Preface (PDF)

pp. xi
Keynote Speaker

POSIX file store in Z/Eves: an experiment in the verified software repository (Abstract)

Leo Freitas , University of York, UK
Jim Woodcock , University of York, UK
Zheng Fu , University of York, UK
pp. 3-14
Real-time Systems

Just-in-Time Certification (Abstract)

John Rushby , SRI International, USA
pp. 15-24

Modular Synthesis of Discrete Controllers (Abstract)

Petra Malik , University of Waikato, New Zealand
Robi Malik , University of Waikato, New Zealand
Steve Reeves , University of Waikato, New Zealand
David Streader , University of Waikato, New Zealand
pp. 25-34
Modeling and Verification

Model Checking-based Verification of Web Application (Abstract)

Hongwei Zeng , Shanghai University, China; Wuhan University, China
Huaikou Miao , Shanghai University, China
pp. 47-55

A light-weight static approach to analyzing UML behavioral properties (Abstract)

Lijun Yu , Colorado State University, USA
Kevin Lano , Kings College, UK
Indrakshi Ray , Colorado State University, USA
Robert B. France , Colorado State University, USA
pp. 56-63

A Formal Model for Compensable Transactions (Abstract)

Huibiao Zhu , East China Normal University, China
Jifeng He , East China Normal University, China
Jing Li , East China Normal University, China
Geguang Pu , East China Normal University, China
pp. 64-73

A Formal Semantic Model of the Semantic Web Service Ontology (WSMO) (Abstract)

Nick Gibbins , University of Southampton, UK
Jun Sun , National University of Singapore, Singapore
Ahmed Saleh , University of Southampton, UK
Terry Payne , University of Southampton, UK
Hai H. Wang , University of Southampton, UK
pp. 74-86
Keynote Speaker

Selecting V&V Technology Combinations: How to Pick a Winner? (Abstract)

Margaret A. Wojcicki , The University of Queensland, Australia
Paul Strooper , The University of Queensland, Australia
pp. 87-96
Safety and Security

A Novel Approach to the Detection of Cheating in Multiplayer Online Games (Abstract)

Howard Chivers , Cranfield University, UK
Richard F. Paige , University of York, UK
Phillip J. Brooke , University of Teesside, UK
Peter Laurens , University of York, UK
pp. 97-106

Reasoning about Nonblocking Concurrency using Reduction (Abstract)

Lindsay Groves , Victoria University of Wellington, New Zealand
pp. 107-116

A Combined Approach for Information Flow Analysis in Fault Tolerant Hardware (Abstract)

Luke Wildman , University of Queensland, Australia
Tim McComb , University of Queensland, Australia
pp. 117-128
Context Awareness and Ubiquitous Computing

The Registry for Sensor Network Discovery (Abstract)

Keung Hae Lee , Korea Aerospace University, Korea
Jiung Han , Korea Aerospace University, Korea
Jeongkyu Park , Korea Aerospace University, Korea
Kibong Kang , Korea Aerospace University, Korea
pp. 129-137

An agent based approach to examining shared situation awareness (Abstract)

Marcus Gallagher , University of Queensland, Australia
Simon Connelly , University of Queensland, Australia
Peter Lindsay , University of Queensland, Australia
pp. 138-147

Product Line Enabled Intelligent Mobile Middleware (Abstract)

Klaus Marius , Hansen University of Aarhus, Denmark
Weishan Zhang , Tongji University, China
Thomas Kunz , Carleton University, Canada
pp. 148-160
Keynote Speaker
Formal Languages

Belief-augmented OWL (BOWL) Engineering the SemanticWeb with Beliefs (Abstract)

Hai Wang , University of Southampton, United Kingdom
Colin Keng-Yan Tan , National University of Singapore, Singapore
Bimlesh Wadhwa , National University of Singapore, Singapore
Yuan Fang Li , National University of Singapore, Singapore
Yuzhang Feng , National University of Singapore, Singapore
pp. 165-174

A Formal Contract Language for Plugin-based Software Engineering (Abstract)

Jens Dietrich , Massey University, New Zealand
Jonathan Giles , Massey University, New Zealand
John Hosking , University of Auckland, New Zealand
pp. 175-184

Linking Object-Z with Spec# (Abstract)

Guanhua He , Durham University, UK
Shengchao Qin , Durham University, UK
pp. 185-196
Software Architecture

Communicating Software Architecture using a Unified Single-View Visualization (Abstract)

Richard Vuduc , Lawrence Livermore National Laboratory
Thomas Panas , Lawrence Livermore National Laboratory
Thomas Epperly , Lawrence Livermore National Laboratory
Andreas Saebjornsen , Lawrence Livermore National Laboratory
Daniel Quinlan , Lawrence Livermore National Laboratory
pp. 217-228
Special Session: Addressing Complexity with Autonomic Systems

A first approach to the closed-form specification and analysis of an autonomic control system (Abstract)

Stephen Knox , UCD Dublin, Ireland
Simon Dobson , UCD Dublin, Ireland
Aaron Quigley , UCD Dublin, Ireland
Eoin Bailey , UCD Dublin, Ireland
Ross Shannon , UCD Dublin, Ireland
pp. 229-237

The Imminent Complexity Quagmire in Pervasive Computing--Autonomic Agents a Solution? (Abstract)

Sarah Eowyn , Johnston University of Ulster, Northern Ireland
Roy Sterritt , University of Ulster, Northern Ireland
Patricia O'Hagan , Core Systems, Belfast, Northern Ireland
Edward Hanna , Core Systems, Belfast, Northern Ireland
pp. 238-250
Special Session: Grand Challenges--Complex Program Verifier

Formalising Flash Memory: First Steps (Abstract)

Jim Woodcock , University of York, UK
Andrew Butterfield , Trinity College Dublin, Ireland
pp. 251-260

Formally Counting Electronic Votes (But Still Only Trusting Paper) (Abstract)

Joeseph Kiniry , University College Dublin, Ireland
pp. 261-269

What Use is Verified Software? (Abstract)

John Rushby , SRI International, USA
pp. 270-276

A Refinement Driven Component-Based Design (Abstract)

Zhenbang Chen , United Nations University
Lu Yang , United Nations University
Anders P. Ravn , University of Aalborg, Denmark
Zhiming Liu , United Nations University
Volker Stolz , United Nations University
pp. 277-289

Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository (Abstract)

Leo Freitas , University of York, UK
Jim Woodcock , University of York, UK
Konstantinos Mokos , University of York, UK
pp. 290-298

What Can the \pi-calculus Tell Us About the Mondex Purse System? (Abstract)

Ken G. Pierce , Newcastle University, UK
Cliff B. Jones , Newcastle University, UK
pp. 300-306

Automated Verification of Shape, Size and Bag Properties (Abstract)

Huu Hai Nguyen , Singapore-MIT Alliance
Shengchao Qin , Durham University, UK
Cristina David , National University of Singapore, Singapore
Wei-Ngan Chin , National University of Singapore, Singapore; Singapore-MIT Alliance
pp. 307-320
Special Session: Advances in the FMICS-jETI Platform for Program Verification

On-the-fly model checking for C programs with extended CADP in FMICS-jETI (Abstract)

Christophe Joubert , Technical University of Valencia, Spain
David Sanán , University of Malaga, Spain
María del Mar Gallardo , University of Malaga, Spain
Pedro Merino , University of Malaga, Spain
pp. 321-329

Parallel Model Checking and the FMICS-jETI Platform (Abstract)

Jirí Barnat , Masaryk University, Czech Republic
Lubos Brim , Masaryk University, Czech Republic
Martin Leucker , Technische Universitat Munchen, Germany
pp. 330-339

The LearnLib in FMICS-jETI (Abstract)

Harald Raffelt , University of Dortmund, Germany
Tiziana Margaria , University of Potsdam, Germany
Martin Leucker , TU Munchen, Germany
Bernhard Steffen , University of Dortmund, Germany
pp. 340-352
Selected Papers from the UML&AADL 2007 Workshop

Managing Complexity of Automotive Electronics Using the EAST-ADL (Abstract)

Carl-Johan Sjöstedt , Royal Institute of Technology, Sweden
DeJiu Chen , Royal Institute of Technology, Sweden
Sébastien Gérard , CEA List, France
Matthias Weber , Carmeq GmbH, Germany
Ramin Tavakoli Kolagari , Technical University of Berlin, Germany
David Servat , CEA List, France
Henrik Lönn , Volvo Technology Corporation, Sweden
Mark-Oliver Reiser , Technical University of Berlin, Germany
Philippe Cuenot , Siemens VDO, France
Martin Törngren , Royal Institute of Technology, Sweden
pp. 353-358

MARTE: Also an UML Profile for Modeling AADL Applications (Abstract)

Robert de Simone , INRIA, France
Sébastien Gérard , CEA LIST, France
Madeleine Faugère , Thales Research and Technology
Thimothée Bourbeau , Thales Research and Technology
pp. 359-364

From PIMs to PSMs (Abstract)

Peter H. Feiler , Carnegie Mellon University
Dio de Niz , Carnegie Mellon University
Bruce A. Lewis , US Army, AMRDEC
Chris Raistrick , Kennedy-Carter
pp. 365-370

The AADL behaviour annex -- experiments and roadmap (Abstract)

David Chemouil , Centre national d'etudes spatiales, Toulouse
Mamoun Filali , IRIT-Universite Paul Sabatier, France
Dave Thomas , EADS Astrium Satellites
Jean-François Rolland , IRIT-Universite Paul Sabatier, France
Ricardo Bedin França , IRIT-Universite Paul Sabatier, France
Jean-Paul Bodeveix , IRIT-Universite Paul Sabatier, France
pp. 377-382
Author Index

Author Index (PDF)

pp. 383
107 ms
(Ver )